--- a/CookBook/Solutions.thy	Wed Mar 18 03:27:15 2009 +0100
+++ b/CookBook/Solutions.thy	Wed Mar 18 18:27:48 2009 +0100
@@ -117,22 +117,18 @@
     | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm
     | _ => Conv.all_conv ctrm)
 
-val add_tac = CSUBGOAL (fn (goal, i) =>
-  let
-    val ctxt = ProofContext.init (Thm.theory_of_cterm goal)
-  in
-    CONVERSION
-      (Conv.params_conv ~1 (fn ctxt =>
-        (Conv.prems_conv ~1 (add_conv ctxt) then_conv
-          Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i
-  end)*}
+fun add_tac ctxt = CSUBGOAL (fn (goal, i) =>
+  CONVERSION
+    (Conv.params_conv ~1 (fn ctxt =>
+       (Conv.prems_conv ~1 (add_conv ctxt) then_conv
+          Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i)*}
 
 text {*
   A test case for this conversion is as follows
 *}
 
 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
-  apply(tactic {* add_tac 1 *})?
+  apply(tactic {* add_tac @{context} 1 *})?
 txt {* 
   where it produces the goal state
   
@@ -197,7 +193,7 @@
 ML{*local
   fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}])
 in
-val c_tac = mk_tac add_tac
+val c_tac = mk_tac (add_tac @{context}) 
 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))
 end*}