# HG changeset patch
# User wenzelm
# Date 1255790441 -7200
# Node ID 15489e162b21250d5621958496c7a863ba3575fd
# Parent  c9fbd4a4d39efd4b98f92841145a989a23ea5186
Method.cheating: check quick_and_dirty here;

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 *)