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