--- 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 _ =

--- a/ProgTutorial/Tactical.thy	Tue Mar 20 09:39:44 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Mon Apr 30 12:33:17 2012 +0100
@@ -1992,8 +1992,7 @@
 let
   val num = HOLogic.mk_number @{typ "nat"} n
   val goal = Logic.mk_equals (t, num)
-  val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @ 
-          @{thms eval_nat_numeral} @ @{thms neg_simps} @ @{thms plus_nat.simps}
+  val num_ss = HOL_ss addsimps @{thms semiring_norm}
 in
   Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
 end*}
@@ -2017,7 +2016,7 @@
 let 
   val ctxt = Simplifier.the_context ss
 in
-  SOME (get_thm ctxt (t, dest_suc_trm t))
+  SOME (get_thm_alt ctxt (t, dest_suc_trm t))
   handle TERM _ => NONE
 end*}
 

Binary file progtutorial.pdf has changed