Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/skip_proof.ML
changeset 32966 5b21661fe618
parent 30288 a32700e45ab3
child 32970 fbd2bb2489a8 
--- a/src/Pure/Isar/skip_proof.ML	Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Sat Oct 17 15:57:51 2009 +0200
@@ -36,7 +36,7 @@
   (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
     (fn args => fn st =>
       if ! quick_and_dirty
-      then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
+      then setmp_CRITICAL quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
       else tac args st);
 
 fun prove_global thy xs asms prop tac =
isabelle