do not fork skipped proofs;
authorwenzelm
Thu, 29 Dec 2011 19:37:24 +0100
changeset 46045 332cb37cfcee
parent 46044 83b53c870efb
child 46046 05392bdd2286
do not fork skipped proofs;
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);