--- a/ProgTutorial/Tactical.thy	Sun Oct 18 08:44:39 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sun Oct 18 21:22:44 2009 +0200
@@ -363,13 +363,13 @@
 
 text {*
   A simple tactic for easy discharge of any proof obligations is 
-  @{ML_ind  cheat_tac in SkipProof}. This tactic corresponds to
+  @{ML_ind  cheat_tac in Skip_Proof}. This tactic corresponds to
   the Isabelle command \isacommand{sorry} and is sometimes useful  
   during the development of tactics.
 *}
 
 lemma shows "False" and "Goldbach_conjecture"  
-apply(tactic {* SkipProof.cheat_tac @{theory} *})
+apply(tactic {* Skip_Proof.cheat_tac @{theory} *})
 txt{*\begin{minipage}{\textwidth}
      @{subgoals [display]}
      \end{minipage}*}