1.1 --- a/src/Pure/Concurrent/par_list.ML	Tue Jul 21 10:23:16 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/par_list.ML	Tue Jul 21 10:24:57 2009 +0200
     1.3 @@ -28,11 +28,8 @@
     1.4  
     1.5  fun raw_map f xs =
     1.6    if Future.enabled () then
     1.7 -    let
     1.8 -      val group = Task_Queue.new_group ();
     1.9 -      val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
    1.10 -      val _ = List.app (ignore o Future.join_result) futures;
    1.11 -    in Future.join_results futures end
    1.12 +    let val group = Task_Queue.new_group ()
    1.13 +    in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
    1.14    else map (Exn.capture f) xs;
    1.15  
    1.16  fun map f xs = Exn.release_first (raw_map f xs);

     2.1 --- a/src/Pure/proofterm.ML	Tue Jul 21 10:23:16 2009 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Tue Jul 21 10:24:57 2009 +0200
     2.3 @@ -37,10 +37,8 @@
     2.4  
     2.5    type oracle = string * term
     2.6    type pthm = serial * (string * term * proof_body future)
     2.7 -  val join_body: proof_body future ->
     2.8 -    {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
     2.9 +  val proof_of: proof_body -> proof
    2.10    val join_proof: proof_body future -> proof
    2.11 -  val proof_of: proof_body -> proof
    2.12    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    2.13    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
    2.14    val join_bodies: proof_body list -> unit
    2.15 @@ -152,10 +150,8 @@
    2.16  type oracle = string * term;
    2.17  type pthm = serial * (string * term * proof_body future);
    2.18  
    2.19 -val join_body = Future.join #> (fn PBody args => args);
    2.20 -val join_proof = #proof o join_body;
    2.21 -
    2.22  fun proof_of (PBody {proof, ...}) = proof;
    2.23 +val join_proof = Future.join #> proof_of;
    2.24  
    2.25  
    2.26  (***** proof atoms *****)
    2.27 @@ -177,13 +173,15 @@
    2.28  
    2.29  fun fold_body_thms f =
    2.30    let
    2.31 -    fun app (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
    2.32 -      if Inttab.defined seen i then (x, seen)
    2.33 -      else
    2.34 -        let
    2.35 -          val body' = Future.join body;
    2.36 -          val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    2.37 -        in (f (name, prop, body') x', seen') end);
    2.38 +    fun app (PBody {thms, ...}) =
    2.39 +     (Future.join_results (map (#3 o #2) thms);
    2.40 +      thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
    2.41 +        if Inttab.defined seen i then (x, seen)
    2.42 +        else
    2.43 +          let
    2.44 +            val body' = Future.join body;
    2.45 +            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    2.46 +          in (f (name, prop, body') x', seen') end));
    2.47    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    2.48  
    2.49  fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
    2.50 @@ -223,13 +221,14 @@
    2.51  val all_oracles_of =
    2.52    let
    2.53      fun collect (PBody {oracles, thms, ...}) =
    2.54 +     (Future.join_results (map (#3 o #2) thms);
    2.55        thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
    2.56          if Inttab.defined seen i then (x, seen)
    2.57          else
    2.58            let
    2.59              val body' = Future.join body;
    2.60              val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
    2.61 -          in (merge_oracles oracles x', seen') end);
    2.62 +          in (merge_oracles oracles x', seen') end));
    2.63    in fn body => #1 (collect body ([], Inttab.empty)) end;
    2.64  
    2.65  fun approximate_proof_body prf =
    2.66 @@ -1342,5 +1341,5 @@
    2.67  
    2.68  end;
    2.69  
    2.70 -structure BasicProofterm : BASIC_PROOFTERM = Proofterm;
    2.71 -open BasicProofterm;
    2.72 +structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;
    2.73 +open Basic_Proofterm;

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