1.1 --- a/src/Pure/thm.ML	Wed Oct 01 08:42:42 2008 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed Oct 01 12:00:00 2008 +0200
     1.3 @@ -1612,8 +1612,17 @@
     1.4  fun add_future thy future = CRITICAL (fn () => change (Futures.get thy) (cons future));
     1.5  
     1.6  fun join_futures thy =
     1.7 -  (case CRITICAL (fn () => ! (Futures.get thy)) of [] => ()
     1.8 -  | futures => (Future.release_results (Future.join_results (rev futures)); join_futures thy));
     1.9 +  let
    1.10 +    val futures = Futures.get thy;
    1.11 +    fun joined () =
    1.12 +     (Future.join_results (rev (! futures));
    1.13 +      CRITICAL (fn () =>
    1.14 +        let
    1.15 +          val (finished, unfinished) = List.partition Future.is_finished (! futures);
    1.16 +          val _ = futures := unfinished;
    1.17 +        in finished end)
    1.18 +      |> Future.join_results |> Exn.release_all |> null);
    1.19 +  in while not (joined ()) do () end;
    1.20  
    1.21  
    1.22  (* promise *)
    1.23 @@ -1658,7 +1667,7 @@
    1.24  
    1.25  fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
    1.26    let
    1.27 -    val _ = Future.release_results (Future.join_results (rev (map #2 promises)));
    1.28 +    val _ = Exn.release_all (Future.join_results (rev (map #2 promises)));
    1.29      val results = map (apsnd Future.join) promises;
    1.30      val proofs = fold (fn (i, Thm (Deriv {proof = prf, ...}, _)) => Inttab.update (i, prf))
    1.31        results Inttab.empty;