src/Pure/Isar/skip_proof.ML
changeset 32966 5b21661fe618
parent 30288 a32700e45ab3
child 32970 fbd2bb2489a8
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Oct 17 15:55:57 2009 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Oct 17 15:57:51 2009 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
     1.5      (fn args => fn st =>
     1.6        if ! quick_and_dirty
     1.7 -      then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
     1.8 +      then setmp_CRITICAL quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
     1.9        else tac args st);
    1.10  
    1.11  fun prove_global thy xs asms prop tac =