diff --git a/src/interpretation.ml b/src/interpretation.ml
index d5adc150ae85d1d0422dd32a5025a65f2c9c42e0..8aa6b79eacd39a418306c5dbebdfa2e3007ef296 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -297,7 +297,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
         ([ Ident.op_get "" ] (* ([]) *), None, vget);
         ([ Ident.op_infix "-" ], None, vminus);
         ([ "length" ], None, length);
-        ([ "L"; "mapi" ], None, mapi);
+        ([ "mapi" ], None, mapi);
       ] );
     ( [ "interpretation" ],
       "NeuralNetwork",
diff --git a/stdlib/interpretation.mlw b/stdlib/interpretation.mlw
index 603276e9db876c87fe5363c826b2f5ae969ff460..68a0d7073228d708da194a9710e25d3ffc1548d8 100644
--- a/stdlib/interpretation.mlw
+++ b/stdlib/interpretation.mlw
@@ -33,23 +33,21 @@ theory Vector
   predicate has_length (v: vector 'a) (i: int)
   predicate valid_index (v: vector 'a) (i: index) = 0 <= i < length v
 
-  scope L
-    function mapi (v: vector 'a) (f: index -> 'a -> 'b) : vector 'b
-    function map (v: vector 'a) (f: 'a -> 'b) : vector 'b
-    function map2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c
+  function mapi (v: vector 'a) (f: index -> 'a -> 'b) : vector 'b
+  function map (v: vector 'a) (f: 'a -> 'b) : vector 'b
+  function map2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c
 
-    predicate forall_ (v: vector 'a) (f: 'a -> bool) =
-      forall i: index. valid_index v i -> f v[i]
+  predicate forall_ (v: vector 'a) (f: 'a -> bool) =
+    forall i: index. valid_index v i -> f v[i]
 
-    predicate forall2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> bool) =
-      length(v1) = length(v2) -> forall i: index. valid_index v1 i -> f v1[i] v2[i]
+  predicate forall2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> bool) =
+    length(v1) = length(v2) -> forall i: index. valid_index v1 i -> f v1[i] v2[i]
 
-    function foreach (v: vector 'a) (f: 'a -> 'b) : vector 'b =
-      map v f
+  function foreach (v: vector 'a) (f: 'a -> 'b) : vector 'b =
+    map v f
 
-    function foreach2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c =
-      map2 v1 v2 f
-  end
+  function foreach2 (v1: vector 'a) (v2: vector 'b) (f: 'a -> 'b -> 'c) : vector 'c =
+    map2 v1 v2 f
 end
 
 theory NeuralNetwork
@@ -70,11 +68,9 @@ theory Dataset
 
   function read_dataset (f: string) (k: format) : dataset 'a 'b
 
-  scope L
-    predicate forall_ (d: dataset 'a 'b) (f: 'a -> 'b -> bool) =
-      Vector.L.forall_ d (fun e -> let a, b = e in f a b)
+  predicate forall_ (d: dataset 'a 'b) (f: 'a -> 'b -> bool) =
+    Vector.forall_ d (fun e -> let a, b = e in f a b)
 
-    function foreach (d: dataset 'a 'b) (f: 'a -> 'b -> 'c) : vector 'c =
-      Vector.L.foreach d (fun e -> let a, b = e in f a b)
-  end
+  function foreach (d: dataset 'a 'b) (f: 'a -> 'b -> 'c) : vector 'c =
+    Vector.foreach d (fun e -> let a, b = e in f a b)
 end
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index be3de19f935271232d2e5c20a6c7db269231b1dc..8591192094f156eba26c4a530922313d44a4557f 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -65,7 +65,7 @@ Test interpret on acasxu
   >     else t
   > 
   >   function denormalize_input (i:input) : input =
-  >     Vector.L.mapi i denormalize_by_index
+  >     Vector.mapi i denormalize_by_index
   > 
   >   function denormalize_output (o: t) : t =
   >     denormalize_t o (7.51888402010059753166615337249822914600372314453125:t) (373.9499200000000200816430151462554931640625:t)
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index cf06a9b7ce8bb6eae08d34d9c0b9b76ba5d982cf..9996b4544ebb90ec070a0730f800f908427f9a1e 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -44,7 +44,7 @@ Test interpret on dataset
   >       advises n perturbed_image l
   > 
   >   predicate robust (n: nn) (d: dataset image label_) (eps: t) =
-  >     Dataset.L.forall_ d (robust_around n eps)
+  >     Dataset.forall_ d (robust_around n eps)
   > 
   >   goal G:
   >     let nn = read_neural_network "TestNetwork.nnet" NNet in