# HG changeset patch
# User wenzelm
# Date 1222367660 -7200
# Node ID 6249297461cbc91b0900c76a8ac59e2345a93bfd
# Parent  0012c6e5347e8e12ce43326e122090949b2290c5
added future_scheduler (from thy_info.ML);
prove: Goal.prove_promise if future_schedule;

diff -r 0012c6e5347e -r 6249297461cb src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Thu Sep 25 20:34:19 2008 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Thu Sep 25 20:34:20 2008 +0200
@@ -5,6 +5,8 @@
 Skipping proofs -- quick_and_dirty mode.
 *)
 
+val future_scheduler = ref false;
+
 signature SKIP_PROOF =
 sig
   val make_thm: theory -> term -> thm
@@ -34,10 +36,11 @@
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 fun prove ctxt xs asms prop 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);
+  (if ! future_scheduler then Goal.prove_promise else 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);
 
 fun prove_global thy xs asms prop tac =
   Drule.standard (prove (ProofContext.init thy) xs asms prop tac);