1.1 --- a/src/Pure/Isar/method.ML	Sat Oct 17 16:34:39 2009 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sat Oct 17 16:40:41 2009 +0200
     1.3 @@ -151,8 +151,10 @@
     1.4  
     1.5  (* cheating *)
     1.6  
     1.7 -fun cheating int ctxt = METHOD (K (setmp_CRITICAL quick_and_dirty (int orelse ! quick_and_dirty)
     1.8 -    (SkipProof.cheat_tac (ProofContext.theory_of ctxt))));
     1.9 +fun cheating int ctxt =
    1.10 +  if int orelse ! quick_and_dirty then
    1.11 +    METHOD (K (Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)))
    1.12 +  else error "Cheating requires quick_and_dirty mode!";
    1.13  
    1.14  
    1.15  (* unfold intro/elim rules *)