# HG changeset patch
# User wenzelm
# Date 1233013332 -3600
# Node ID d01bada1df333cb5bcbd2e7eaddcc2255d270466
# Parent  31d14e9fa0da952c0efa2825e56eb609477a7516
thm_proof: replaced lazy by composed futures;

diff -r 31d14e9fa0da -r d01bada1df33 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Jan 27 00:29:37 2009 +0100
+++ b/src/Pure/proofterm.ML	Tue Jan 27 00:42:12 2009 +0100
@@ -110,7 +110,7 @@
   val promise_proof: theory -> serial -> term -> proof
   val fulfill_proof: theory -> (serial * proof) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> term list -> term ->
-    (serial * proof) list lazy -> proof_body -> pthm * proof
+    (serial * proof future) list -> proof_body -> pthm * proof
   val get_name: term list -> term -> proof -> string
 
   (** rewriting on proof terms **)
@@ -1245,8 +1245,9 @@
       else MinProof;
 
     fun new_prf () = (serial (), name, prop,
-      Future.fork_pri ~2 (fn () => fulfill_proof thy (Lazy.force promises)
-        (PBody {oracles = oracles0, thms = thms0, proof = proof0})));
+      Future.fork_deps (map snd promises) (fn () =>
+        fulfill_proof thy (map (apsnd Future.join) promises)
+          (PBody {oracles = oracles0, thms = thms0, proof = proof0})));
 
     val (i, name, prop, body') =
       (case strip_combt (fst (strip_combP prf)) of
diff -r 31d14e9fa0da -r d01bada1df33 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jan 27 00:29:37 2009 +0100
+++ b/src/Pure/thm.ML	Tue Jan 27 00:42:12 2009 +0100
@@ -1658,7 +1658,7 @@
     val {thy_ref, hyps, prop, tpairs, ...} = args;
     val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
 
-    val ps = Lazy.lazy (fn () => map (apsnd (proof_of o Future.join)) promises);
+    val ps = map (apsnd (Future.map proof_of)) promises;
     val thy = Theory.deref thy_ref;
     val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;