prove: setmp quick_and_dirty (avoids race condition);

--- 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;