# HG changeset patch
# User wenzelm
# Date 1188578797 -7200
# Node ID 8d5326f0098b4e642ae36708cc79ea18665c9a44
# Parent  7a2b201458880e8174cdfe0bec6171bfcca58bfa
prove: setmp quick_and_dirty (avoids race condition);

diff -r 7a2b20145888 -r 8d5326f0098b src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Fri Aug 31 18:46:35 2007 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Fri Aug 31 18:46:37 2007 +0200
@@ -36,7 +36,9 @@
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 fun prove ctxt xs asms prop tac =
-  Goal.prove ctxt xs asms prop
-    (if ! quick_and_dirty then (K (cheat_tac (ProofContext.theory_of ctxt))) else tac);
+  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
+    else tac args st);
 
 end;