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)