# HG changeset patch
# User wenzelm
# Date 1325183844 -3600
# Node ID 332cb37cfceec5e83bfc1299cef25b63793526b3
# Parent  83b53c870efb00b91a9682c2a88b33491e47866c
do not fork skipped proofs;

diff -r 83b53c870efb -r 332cb37cfcee src/Pure/Isar/skip_proof.ML
--- 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);