# HG changeset patch
# User wenzelm
# Date 1227043536 -3600
# Node ID 648f01ec17940942ce5ebe16b3371d25b29a01f6
# Parent  9c6025c721d7a1ec8a5b92d03716c1e5eae82abc
fulfill_proof/thm_proof: commuted lazyness;
join_futures: Exn.release_all is back again (still required for implicit join of Toplevel.excursion);

diff -r 9c6025c721d7 -r 648f01ec1794 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Nov 18 22:25:30 2008 +0100
+++ b/src/Pure/thm.ML	Tue Nov 18 22:25:36 2008 +0100
@@ -1614,7 +1614,7 @@
           val (finished, unfinished) = List.partition Future.is_finished (! futures);
           val _ = futures := unfinished;
         in finished end)
-      |> Future.join_results |> null);
+      |> Future.join_results |> Exn.release_all |> null);
   in while not (joined ()) do () end;
 
 
@@ -1664,7 +1664,7 @@
 fun proof_body_of (Thm (Deriv {all_promises, promises, body}, {thy_ref, ...})) =
   let
     val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
-    val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises;
+    val ps = map (apsnd (raw_proof_of o Future.join)) promises;
   in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
 
 val proof_of = Proofterm.proof_of o proof_body_of;
@@ -1682,8 +1682,7 @@
     val {thy_ref, hyps, prop, tpairs, ...} = args;
     val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
 
-    val ps =
-      map (apsnd (fn future => Lazy.lazy (fn () => proof_of (Future.join future)))) promises;
+    val ps = Lazy.lazy (fn () => map (apsnd (proof_of o Future.join)) promises);
     val thy = Theory.deref thy_ref;
     val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
     val der' = make_deriv [] [] [] [pthm] proof;