diff -r b90109b2487c -r 83db706d7771 src/Tools/Spec_Check/spec_check.ML
--- a/src/Tools/Spec_Check/spec_check.ML	Tue Mar 01 22:11:36 2016 +0100
+++ b/src/Tools/Spec_Check/spec_check.ML	Tue Mar 01 22:49:33 2016 +0100
@@ -128,10 +128,10 @@
   let
     val return = Unsynchronized.ref "return"
     val context : ML_Compiler0.context =
-     {name_space = #name_space ML_Env.local_context,
-      here = #here ML_Env.local_context,
+     {name_space = #name_space ML_Env.context,
+      here = #here ML_Env.context,
       print = fn r => return := r,
-      error = #error ML_Env.local_context}
+      error = #error ML_Env.context}
     val _ =
       Context.setmp_thread_data (SOME (Context.Proof ctxt))
         (fn () =>
@@ -145,7 +145,7 @@
 fun run_test ctxt s =
   Context.setmp_thread_data (SOME (Context.Proof ctxt))
     (fn () =>
-      ML_Compiler0.use_text ML_Env.local_context
+      ML_Compiler0.use_text ML_Env.context
         {line = 0, file = "generated code", verbose = false, debug = false} s) ();
 
 (*split input into tokens*)