src/Tools/Code/code_runtime.ML

--- a/src/Tools/Code/code_runtime.ML	Tue Mar 01 22:11:36 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML	Tue Mar 01 22:49:33 2016 +0100
@@ -82,7 +82,7 @@
 fun exec ctxt verbose code =
  (if Config.get ctxt trace then tracing code else ();
   ML_Context.exec (fn () =>
-    ML_Compiler0.use_text ML_Env.local_context
+    ML_Compiler0.use_text ML_Env.context
       {line = 0, file = "generated code", verbose = verbose, debug = false} code));
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
@@ -503,7 +503,7 @@
 
 fun notify_val (string, value) = 
   let
-    val _ = #enterVal ML_Env.local_name_space (string, value);
+    val _ = #enterVal ML_Env.name_space (string, value);
     val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
   in () end;
 
@@ -511,27 +511,27 @@
 
 val notifying_context : ML_Compiler0.context =
  {name_space =
-   {lookupVal    = #lookupVal ML_Env.local_name_space,
-    lookupType   = #lookupType ML_Env.local_name_space,
-    lookupFix    = #lookupFix ML_Env.local_name_space,
-    lookupStruct = #lookupStruct ML_Env.local_name_space,
-    lookupSig    = #lookupSig ML_Env.local_name_space,
-    lookupFunct  = #lookupFunct ML_Env.local_name_space,
+   {lookupVal    = #lookupVal ML_Env.name_space,
+    lookupType   = #lookupType ML_Env.name_space,
+    lookupFix    = #lookupFix ML_Env.name_space,
+    lookupStruct = #lookupStruct ML_Env.name_space,
+    lookupSig    = #lookupSig ML_Env.name_space,
+    lookupFunct  = #lookupFunct ML_Env.name_space,
     enterVal     = notify_val,
     enterType    = abort,
     enterFix     = abort,
     enterStruct  = abort,
     enterSig     = abort,
     enterFunct   = abort,
-    allVal       = #allVal ML_Env.local_name_space,
-    allType      = #allType ML_Env.local_name_space,
-    allFix       = #allFix ML_Env.local_name_space,
-    allStruct    = #allStruct ML_Env.local_name_space,
-    allSig       = #allSig ML_Env.local_name_space,
-    allFunct     = #allFunct ML_Env.local_name_space},
-  here = #here ML_Env.local_context,
-  print = #print ML_Env.local_context,
-  error = #error ML_Env.local_context};
+    allVal       = #allVal ML_Env.name_space,
+    allType      = #allType ML_Env.name_space,
+    allFix       = #allFix ML_Env.name_space,
+    allStruct    = #allStruct ML_Env.name_space,
+    allSig       = #allSig ML_Env.name_space,
+    allFunct     = #allFunct ML_Env.name_space},
+  here = #here ML_Env.context,
+  print = #print ML_Env.context,
+  error = #error ML_Env.context};
 
 in