1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Mar 24 15:43:13 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 24 15:43:37 2009 +0100
     1.3 @@ -295,28 +295,28 @@
     1.4  
     1.5  (* use ML text *)
     1.6  
     1.7 -fun inherit_env (context as Context.Proof lthy) =
     1.8 +fun propagate_env (context as Context.Proof lthy) =
     1.9        Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
    1.10 -  | inherit_env context = context;
    1.11 +  | propagate_env context = context;
    1.12  
    1.13 -fun inherit_env_prf prf = Proof.map_contexts
    1.14 +fun propagate_env_prf prf = Proof.map_contexts
    1.15    (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
    1.16  
    1.17  val _ =
    1.18    OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
    1.19 -    (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> inherit_env)));
    1.20 +    (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
    1.21  
    1.22  val _ =
    1.23    OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl)
    1.24      (P.ML_source >> (fn (txt, pos) =>
    1.25        Toplevel.generic_theory
    1.26 -        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env)));
    1.27 +        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
    1.28  
    1.29  val _ =
    1.30    OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl)
    1.31      (P.ML_source >> (fn (txt, pos) =>
    1.32        Toplevel.proof (Proof.map_context (Context.proof_map
    1.33 -        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)));
    1.34 +        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)));
    1.35  
    1.36  val _ =
    1.37    OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag)