--- a/ProgTutorial/Solutions.thy	Thu Mar 19 23:21:26 2009 +0100
+++ b/ProgTutorial/Solutions.thy	Sat Mar 21 12:35:03 2009 +0100
@@ -146,12 +146,8 @@
   simplified. We have to be careful to set up the goal so that
   other parts of the simplifier do not interfere. For this we construct an
   unprovable goal which, after simplification, we are going to ``prove'' with
-  the help of the lemma:
-*}
+  the help of ``\isacommand{sorry}'', that is the method @{ML SkipProof.cheat_tac}
 
-lemma cheat: "A" sorry
-
-text {*
   For constructing test cases, we first define a function that returns a 
   complete binary tree whose leaves are numbers and the nodes are 
   additions.
@@ -187,11 +183,11 @@
   Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
   two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,
   respectively. The idea is to first apply the conversion (respectively simproc) and 
-  then prove the remaining goal using the @{thm [source] cheat}-lemma.
+  then prove the remaining goal using @{ML "cheat_tac" in SkipProof}.
 *}
 
 ML{*local
-  fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}])
+  fun mk_tac tac = timing_wrapper (EVERY1 [tac, K (SkipProof.cheat_tac @{theory})])
 in
 val c_tac = mk_tac (add_tac @{context}) 
 val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))