# HG changeset patch
# User wenzelm
# Date 1243862760 -7200
# Node ID ffa5356cc34308c65223b2f24c7dc20b6142b146
# Parent  deddd77112b7b08d9ff0a1df29dd915f689e66b4
ML_Env;

diff -r deddd77112b7 -r ffa5356cc343 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -296,11 +296,11 @@
 (* use ML text *)
 
 fun propagate_env (context as Context.Proof lthy) =
-      Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
+      Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
   | propagate_env context = context;
 
 fun propagate_env_prf prf = Proof.map_contexts
-  (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
+  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
 
 val _ =
   OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
diff -r deddd77112b7 -r ffa5356cc343 src/Pure/ML/ml_test.ML
--- a/src/Pure/ML/ml_test.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Pure/ML/ml_test.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -24,7 +24,7 @@
 );
 
 fun inherit_env context =
-  ML_Context.inherit_env context #>
+  ML_Env.inherit context #>
   Extra_Env.put (Extra_Env.get context);
 
 fun register_tokens toks context =
@@ -155,7 +155,7 @@
         error (output ()); raise exn);
   in if verbose then print (output ()) else () end;
 
-val eval = use_text ML_Context.local_context;
+val eval = use_text ML_Env.local_context;
 
 
 (* ML test command *)
diff -r deddd77112b7 -r ffa5356cc343 src/Tools/Compute_Oracle/am_compiler.ML
--- a/src/Tools/Compute_Oracle/am_compiler.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_compiler.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -185,7 +185,7 @@
 
     in
 	compiled_rewriter := NONE;	
-	use_text ML_Context.local_context (1, "") false (!buffer);
+	use_text ML_Env.local_context (1, "") false (!buffer);
 	case !compiled_rewriter of 
 	    NONE => raise (Compile "cannot communicate with compiled function")
 	  | SOME r => (compiled_rewriter := NONE; r)
diff -r deddd77112b7 -r ffa5356cc343 src/Tools/Compute_Oracle/am_sml.ML
--- a/src/Tools/Compute_Oracle/am_sml.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_sml.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -492,7 +492,7 @@
 
 fun writeTextFile name s = File.write (Path.explode name) s
 
-fun use_source src = use_text ML_Context.local_context (1, "") false src
+fun use_source src = use_text ML_Env.local_context (1, "") false src
     
 fun compile cache_patterns const_arity eqs = 
     let
diff -r deddd77112b7 -r ffa5356cc343 src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Mon Jun 01 15:26:00 2009 +0200
@@ -1081,7 +1081,7 @@
 fun isar_seri_sml module_name =
   Code_Target.parse_args (Scan.succeed ())
   #> (fn () => serialize_ml target_SML
-      (SOME (use_text ML_Context.local_context (1, "generated code") false))
+      (SOME (use_text ML_Env.local_context (1, "generated code") false))
       pr_sml_module pr_sml_stmt module_name);
 
 fun isar_seri_ocaml module_name =