prefer simultaneous join -- for improved scheduling;

--- a/src/Pure/Concurrent/par_list.ML	Tue Jul 21 10:23:16 2009 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Tue Jul 21 10:24:57 2009 +0200
@@ -28,11 +28,8 @@
 
 fun raw_map f xs =
   if Future.enabled () then
-    let
-      val group = Task_Queue.new_group ();
-      val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
-      val _ = List.app (ignore o Future.join_result) futures;
-    in Future.join_results futures end
+    let val group = Task_Queue.new_group ()
+    in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
   else map (Exn.capture f) xs;
 
 fun map f xs = Exn.release_first (raw_map f xs);

--- a/src/Pure/proofterm.ML	Tue Jul 21 10:23:16 2009 +0200
+++ b/src/Pure/proofterm.ML	Tue Jul 21 10:24:57 2009 +0200
@@ -37,10 +37,8 @@
 
   type oracle = string * term
   type pthm = serial * (string * term * proof_body future)
-  val join_body: proof_body future ->
-    {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
+  val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
-  val proof_of: proof_body -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
   val join_bodies: proof_body list -> unit
@@ -152,10 +150,8 @@
 type oracle = string * term;
 type pthm = serial * (string * term * proof_body future);
 
-val join_body = Future.join #> (fn PBody args => args);
-val join_proof = #proof o join_body;
-
 fun proof_of (PBody {proof, ...}) = proof;
+val join_proof = Future.join #> proof_of;
 
 
 (***** proof atoms *****)
@@ -177,13 +173,15 @@
 
 fun fold_body_thms f =
   let
-    fun app (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
-      if Inttab.defined seen i then (x, seen)
-      else
-        let
-          val body' = Future.join body;
-          val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
-        in (f (name, prop, body') x', seen') end);
+    fun app (PBody {thms, ...}) =
+     (Future.join_results (map (#3 o #2) thms);
+      thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+        if Inttab.defined seen i then (x, seen)
+        else
+          let
+            val body' = Future.join body;
+            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
+          in (f (name, prop, body') x', seen') end));
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
 
 fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
@@ -223,13 +221,14 @@
 val all_oracles_of =
   let
     fun collect (PBody {oracles, thms, ...}) =
+     (Future.join_results (map (#3 o #2) thms);
       thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
         if Inttab.defined seen i then (x, seen)
         else
           let
             val body' = Future.join body;
             val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
-          in (merge_oracles oracles x', seen') end);
+          in (merge_oracles oracles x', seen') end));
   in fn body => #1 (collect body ([], Inttab.empty)) end;
 
 fun approximate_proof_body prf =
@@ -1342,5 +1341,5 @@
 
 end;
 
-structure BasicProofterm : BASIC_PROOFTERM = Proofterm;
-open BasicProofterm;
+structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;
+open Basic_Proofterm;

--- a/src/Pure/thm.ML	Tue Jul 21 10:23:16 2009 +0200
+++ b/src/Pure/thm.ML	Tue Jul 21 10:24:57 2009 +0200
@@ -1612,8 +1612,9 @@
 fun raw_body (Thm (Deriv {body, ...}, _)) = body;
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
-  let val ps = map (apsnd (fulfill_body o Future.join)) promises
-  in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
+  Pt.fulfill_proof (Theory.deref thy_ref)
+    (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
+and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
 
 fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
 val proof_of = Pt.proof_of o proof_body_of;
@@ -1652,7 +1653,7 @@
     val _ = null hyps orelse err "bad hyps";
     val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
     val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
-    val _ = List.app (ignore o fulfill_body o Future.join o #2) promises;
+    val _ = fulfill_bodies (map #2 promises);
   in thm end;
 
 fun future future_thm ct =