1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Jun 01 15:26:00 2009 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Jun 01 15:26:00 2009 +0200
     1.3 @@ -296,11 +296,11 @@
     1.4  (* use ML text *)
     1.5  
     1.6  fun propagate_env (context as Context.Proof lthy) =
     1.7 -      Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
     1.8 +      Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
     1.9    | propagate_env context = context;
    1.10  
    1.11  fun propagate_env_prf prf = Proof.map_contexts
    1.12 -  (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
    1.13 +  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
    1.14  
    1.15  val _ =
    1.16    OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)

     2.1 --- a/src/Pure/ML/ml_test.ML	Mon Jun 01 15:26:00 2009 +0200
     2.2 +++ b/src/Pure/ML/ml_test.ML	Mon Jun 01 15:26:00 2009 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4  );
     2.5  
     2.6  fun inherit_env context =
     2.7 -  ML_Context.inherit_env context #>
     2.8 +  ML_Env.inherit context #>
     2.9    Extra_Env.put (Extra_Env.get context);
    2.10  
    2.11  fun register_tokens toks context =
    2.12 @@ -155,7 +155,7 @@
    2.13          error (output ()); raise exn);
    2.14    in if verbose then print (output ()) else () end;
    2.15  
    2.16 -val eval = use_text ML_Context.local_context;
    2.17 +val eval = use_text ML_Env.local_context;
    2.18  
    2.19  
    2.20  (* ML test command *)

     3.1 --- a/src/Tools/Compute_Oracle/am_compiler.ML	Mon Jun 01 15:26:00 2009 +0200
     3.2 +++ b/src/Tools/Compute_Oracle/am_compiler.ML	Mon Jun 01 15:26:00 2009 +0200
     3.3 @@ -185,7 +185,7 @@
     3.4  
     3.5      in
     3.6  	compiled_rewriter := NONE;	
     3.7 -	use_text ML_Context.local_context (1, "") false (!buffer);
     3.8 +	use_text ML_Env.local_context (1, "") false (!buffer);
     3.9  	case !compiled_rewriter of 
    3.10  	    NONE => raise (Compile "cannot communicate with compiled function")
    3.11  	  | SOME r => (compiled_rewriter := NONE; r)

     4.1 --- a/src/Tools/Compute_Oracle/am_sml.ML	Mon Jun 01 15:26:00 2009 +0200
     4.2 +++ b/src/Tools/Compute_Oracle/am_sml.ML	Mon Jun 01 15:26:00 2009 +0200
     4.3 @@ -492,7 +492,7 @@
     4.4  
     4.5  fun writeTextFile name s = File.write (Path.explode name) s
     4.6  
     4.7 -fun use_source src = use_text ML_Context.local_context (1, "") false src
     4.8 +fun use_source src = use_text ML_Env.local_context (1, "") false src
     4.9      
    4.10  fun compile cache_patterns const_arity eqs = 
    4.11      let

     5.1 --- a/src/Tools/code/code_ml.ML	Mon Jun 01 15:26:00 2009 +0200
     5.2 +++ b/src/Tools/code/code_ml.ML	Mon Jun 01 15:26:00 2009 +0200
     5.3 @@ -1081,7 +1081,7 @@
     5.4  fun isar_seri_sml module_name =
     5.5    Code_Target.parse_args (Scan.succeed ())
     5.6    #> (fn () => serialize_ml target_SML
     5.7 -      (SOME (use_text ML_Context.local_context (1, "generated code") false))
     5.8 +      (SOME (use_text ML_Env.local_context (1, "generated code") false))
     5.9        pr_sml_module pr_sml_stmt module_name);
    5.10  
    5.11  fun isar_seri_ocaml module_name =