diff -r 0951d6cec68c -r 3c0f53eae166 src/Tools/Spec_Check/spec_check.ML
--- a/src/Tools/Spec_Check/spec_check.ML	Thu Apr 07 15:32:47 2016 +0200
+++ b/src/Tools/Spec_Check/spec_check.ML	Thu Apr 07 16:53:43 2016 +0200
@@ -136,7 +136,7 @@
     val _ =
       Context.setmp_generic_context (SOME (Context.Proof ctxt))
         (fn () =>
-          ML_Compiler0.use_text context
+          ML_Compiler0.ML context
             {line = 0, file = "generated code", verbose = true, debug = false} s) ()
   in
     Gen_Construction.parse_pred (! return)
@@ -146,7 +146,7 @@
 fun run_test ctxt s =
   Context.setmp_generic_context (SOME (Context.Proof ctxt))
     (fn () =>
-      ML_Compiler0.use_text ML_Env.context
+      ML_Compiler0.ML ML_Env.context
         {line = 0, file = "generated code", verbose = false, debug = false} s) ();
 
 (*split input into tokens*)