Fix parsing issue in VectorProg

CakeML · Dec 1, 2018 · d2315e4 · d2315e4
1 parent 73391fa
commit d2315e4
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/basis/VectorProgScript.sml b/basis/VectorProgScript.sml
@@ -2,7 +2,8 @@
   Module about the built-in 'a vector.
 *)
 open preamble ml_translatorLib ml_translatorTheory ml_progLib
-    mlvectorTheory ListProgTheory basisFunctionsLib
+     ListProgTheory basisFunctionsLib;
+open mlvectorTheory;
 
 val _ = new_theory"VectorProg"
 
@@ -16,8 +17,8 @@ val _ = ml_prog_update (add_dec
   ``Dtabbrev unknown_loc ["'a"] "vector" (Atapp [Atvar "'a"] (Short "vector"))`` I);
 
 val _ = trans "fromList" `Vector`
-val _ = trans "length" `length`
-val _ = trans "sub" `sub`
+val _ = trans "length" `regexp_compiler$length`
+val _ = trans "sub" `regexp_compiler$sub`
 
 
 val _ = next_ml_names := ["tabulate"];