--- a/ProgTutorial/Solutions.thy	Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/Solutions.thy	Fri Apr 19 11:09:18 2013 +0100
@@ -239,9 +239,8 @@
   Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1))
 end
 
-fun add_sp_aux ss t =
+fun add_sp_aux ctxt t =
 let 
-  val ctxt = Simplifier.the_context ss
   val t' = term_of t
 in
   SOME (get_sum_thm ctxt t' (dest_sum t'))
@@ -255,7 +254,7 @@
 text {* and a test case is the lemma *}
 
 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)"
-  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *})
+  apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [@{simproc add_sp}]) 1 *})
 txt {* 
   where the simproc produces the goal state
   
@@ -348,21 +347,23 @@
   then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
 *}
 
+ML Skip_Proof.cheat_tac
+
 ML %grayML{*local
   fun mk_tac tac = 
-        timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})])
+        timing_wrapper (EVERY1 [tac, Skip_Proof.cheat_tac])
 in
-  val c_tac = mk_tac (add_tac @{context}) 
-  val s_tac = mk_tac (simp_tac 
-                       (HOL_basic_ss addsimprocs [@{simproc add_sp}]))
+  fun c_tac ctxt = mk_tac (add_tac ctxt) 
+  fun s_tac ctxt = mk_tac (simp_tac 
+    (put_simpset HOL_basic_ss ctxt addsimprocs [@{simproc add_sp}]))
 end*}
 
 text {*
   This is all we need to let the conversion run against the simproc:
 *}
 
-ML %grayML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)
-val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}
+ML %grayML{*val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => c_tac context)
+val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => s_tac context)*}
 
 text {*
   If you do the exercise, you can see that both ways of simplifying additions