diff -r 7e25716c3744 -r 4b105b97069c ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Tue Mar 20 09:39:44 2012 +0000
+++ b/ProgTutorial/Base.thy	Mon Apr 30 12:33:17 2012 +0100
@@ -85,32 +85,23 @@
 *}
 
 ML {*
-fun propagate_env (context as Context.Proof lthy) =
-      Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy)
-  | propagate_env context = context
-
-fun propagate_env_prf prf = Proof.map_contexts
-  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf
+val _ =
+  Outer_Syntax.command ("ML", Keyword.tag "TutorialML" Keyword.thy_decl)
+    "ML text within theory or local theory"
+    (Parse.ML_source >> (fn (txt, pos) =>
+      Toplevel.generic_theory
+        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
+          Local_Theory.propagate_ml_env #> Context.map_theory (write_file_ml_blk txt))))
 *}
 
 ML {*
 val _ =
-  Outer_Syntax.command ("ML", Keyword.tag "TutorialML" Keyword.thy_decl) "eval ML text within theory"
-    (Parse.position Parse.text >> 
-      (fn (txt, pos) =>
-        Toplevel.generic_theory
-         (ML_Context.exec 
-           (fn () => ML_Context.eval_text true pos txt) 
-              #> propagate_env #> Context.map_theory (write_file_ml_blk txt))))
+  Outer_Syntax.command ("ML_prf", Keyword.tag "TutorialMLprf" Keyword.prf_decl) "ML text within proof"
+    (Parse.ML_source >> (fn (txt, pos) =>
+      Toplevel.proof (Proof.map_context (Context.proof_map
+        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
 *}
 
-ML {*
-val _ =
-  Outer_Syntax.command ("ML_prf", Keyword.tag "TutorialMLprf" Keyword.prf_decl) "ML text within proof" 
-    (Parse.ML_source >> (fn (txt, pos) =>
-      Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)))
-*}
 
 ML {*
 val _ =