diff -r c9fbd4a4d39e -r 15489e162b21 src/Pure/Isar/method.ML --- 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 *)