# HG changeset patch
# User wenzelm
# Date 1233062931 -3600
# Node ID be22ba2144757e2386ca3d079a746d323edc0cd0
# Parent  08d462dbb1a9ded103c641d13aa04dd41073a5f8
thm_proof: recovered single-threaded version;

diff -r 08d462dbb1a9 -r be22ba214475 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Jan 27 13:52:32 2009 +0100
+++ b/src/Pure/proofterm.ML	Tue Jan 27 14:28:51 2009 +0100
@@ -1227,6 +1227,11 @@
         val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
       in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
+fun fulfill_proof_future _ [] body = Future.value body
+  | fulfill_proof_future thy promises body =
+      Future.fork_deps (map snd promises) (fn () =>
+        fulfill_proof thy (map (apsnd Future.join) promises) body);
+
 
 (***** theorems *****)
 
@@ -1243,12 +1248,9 @@
       if ! proofs = 2 then
         #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
       else MinProof;
+    val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
 
-    fun new_prf () = (serial (), name, prop,
-      Future.fork_deps (map snd promises) (fn () =>
-        fulfill_proof thy (map (apsnd Future.join) promises)
-          (PBody {oracles = oracles0, thms = thms0, proof = proof0})));
-
+    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
     val (i, name, prop, body') =
       (case strip_combt (fst (strip_combP prf)) of
         (PThm (i, ((old_name, prop', NONE), body')), args') =>