--- a/ProgTutorial/Solutions.thy	Sun Oct 18 08:44:39 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Sun Oct 18 21:22:44 2009 +0200
@@ -272,7 +272,7 @@
   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 ``\isacommand{sorry}'', that is the method @{ML SkipProof.cheat_tac}
+  the help of ``\isacommand{sorry}'', that is the method @{ML Skip_Proof.cheat_tac}
 
   For constructing test cases, we first define a function that returns a 
   complete binary tree whose leaves are numbers and the nodes are 
@@ -309,12 +309,12 @@
   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 @{ML "cheat_tac" in SkipProof}.
+  then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
 *}
 
 ML{*local
   fun mk_tac tac = 
-        timing_wrapper (EVERY1 [tac, K (SkipProof.cheat_tac @{theory})])
+        timing_wrapper (EVERY1 [tac, K (Skip_Proof.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}]))