--- a/ProgTutorial/Base.thy	Wed Mar 25 15:09:04 2009 +0100
+++ b/ProgTutorial/Base.thy	Thu Mar 26 19:00:51 2009 +0000
@@ -8,11 +8,28 @@
 (* to have a special tag for text enclosed in ML *)
 ML {*
 
+fun inherit_env (context as Context.Proof lthy) =
+      Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
+  | inherit_env context = context;
+
+fun inherit_env_prf prf = Proof.map_contexts
+  (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf
+
 val _ =
   OuterSyntax.command "ML" "eval ML text within theory"
     (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
     (OuterParse.ML_source >> (fn (txt, pos) =>
-      Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
+      Toplevel.generic_theory
+        (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env)));
+
+
+val _ =
+  OuterSyntax.command "ML_prf" "ML text within proof" 
+    (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
+    (OuterParse.ML_source >> (fn (txt, pos) =>
+      Toplevel.proof (Proof.map_context (Context.proof_map
+        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)))
+
 *}
 (*
 ML {*