# HG changeset patch
# User wenzelm
# Date 1456868973 -3600
# Node ID 83db706d7771404c66b607bab2b3958b85e8861a
# Parent  b90109b2487c897668f07aeb22c5f11f7f1e8ebb
tuned signature;

diff -r b90109b2487c -r 83db706d7771 src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Tue Mar 01 22:11:36 2016 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Tue Mar 01 22:49:33 2016 +0100
@@ -184,7 +184,7 @@
 
     in
         compiled_rewriter := NONE;      
-        ML_Compiler0.use_text ML_Env.local_context
+        ML_Compiler0.use_text ML_Env.context
           {line = 1, file = "", verbose = false, debug = false} (!buffer);
         case !compiled_rewriter of 
             NONE => raise (Compile "cannot communicate with compiled function")
diff -r b90109b2487c -r 83db706d7771 src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Tue Mar 01 22:11:36 2016 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Tue Mar 01 22:49:33 2016 +0100
@@ -486,7 +486,7 @@
 fun writeTextFile name s = File.write (Path.explode name) s
 
 fun use_source src =
-  ML_Compiler0.use_text ML_Env.local_context
+  ML_Compiler0.use_text ML_Env.context
     {line = 1, file = "", verbose = false, debug = false} src
     
 fun compile rules = 
diff -r b90109b2487c -r 83db706d7771 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Mar 01 22:11:36 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Mar 01 22:49:33 2016 +0100
@@ -206,7 +206,7 @@
 
 fun exec verbose code =
   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 with_overlord_dir name f =
diff -r b90109b2487c -r 83db706d7771 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Mar 01 22:11:36 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Tue Mar 01 22:49:33 2016 +0100
@@ -149,7 +149,7 @@
 fun eval (flags: flags) pos toks =
   let
     val _ = Secure.deny_ml ();
-    val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags};
+    val space = ML_Env.make_name_space {SML = #SML flags, exchange = #exchange flags};
     val opt_context = Context.thread_data ();
 
 
diff -r b90109b2487c -r 83db706d7771 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Tue Mar 01 22:11:36 2016 +0100
+++ b/src/Pure/ML/ml_env.ML	Tue Mar 01 22:49:33 2016 +0100
@@ -13,9 +13,9 @@
     Context.generic -> Context.generic
   val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option
   val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
-  val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
-  val local_context: ML_Compiler0.context
-  val local_name_space: ML_Name_Space.T
+  val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
+  val context: ML_Compiler0.context
+  val name_space: ML_Name_Space.T
   val check_functor: string -> unit
 end
 
@@ -108,7 +108,7 @@
             in (val2, type2, fixity2, structure2, signature2, functor2) end);
     in make_data (bootstrap, tables', sml_tables', breakpoints) end);
 
-fun name_space {SML, exchange} : ML_Name_Space.T =
+fun make_name_space {SML, exchange} : ML_Name_Space.T =
   let
     fun lookup sel1 sel2 name =
       if SML then
@@ -162,15 +162,15 @@
     allFunct     = all #6 #allFunct}
   end;
 
-val local_context: ML_Compiler0.context =
- {name_space = name_space {SML = false, exchange = false},
+val context: ML_Compiler0.context =
+ {name_space = make_name_space {SML = false, exchange = false},
   here = Position.here oo Position.line_file,
   print = writeln,
   error = error};
 
-val local_name_space = #name_space local_context;
+val name_space = #name_space context;
 
-val is_functor = is_some o #lookupFunct local_name_space;
+val is_functor = is_some o #lookupFunct name_space;
 
 fun check_functor name =
   if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
diff -r b90109b2487c -r 83db706d7771 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
 
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*)