--- a/src/Pure/Isar/skip_proof.ML Thu Dec 29 18:27:17 2011 +0100
+++ b/src/Pure/Isar/skip_proof.ML Thu Dec 29 19:37:24 2011 +0100
@@ -33,11 +33,9 @@
ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
fun prove ctxt xs asms prop tac =
- (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
- (fn args => fn st =>
- if ! quick_and_dirty
- then cheat_tac (Proof_Context.theory_of ctxt) st
- else tac args st);
+ if ! quick_and_dirty then
+ Goal.prove ctxt xs asms prop (fn _ => cheat_tac (Proof_Context.theory_of ctxt))
+ else (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop tac;
fun prove_global thy xs asms prop tac =
Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);