--- a/src/Pure/Isar/method.ML Sat Oct 17 16:34:39 2009 +0200
+++ b/src/Pure/Isar/method.ML Sat Oct 17 16:40:41 2009 +0200
@@ -151,8 +151,10 @@
(* cheating *)
-fun cheating int ctxt = METHOD (K (setmp_CRITICAL quick_and_dirty (int orelse ! quick_and_dirty)
- (SkipProof.cheat_tac (ProofContext.theory_of ctxt))));
+fun cheating int ctxt =
+ if int orelse ! quick_and_dirty then
+ METHOD (K (Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)))
+ else error "Cheating requires quick_and_dirty mode!";
(* unfold intro/elim rules *)