join earlier promises first;
authorwenzelm
Sun Sep 28 12:42:35 2008 +0200 (2008-09-28)
changeset 283911a4804fc2216
parent 28390 0b9fb63b8e1d
child 28392 d10839c203bd
join earlier promises first;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Sun Sep 28 12:23:45 2008 +0200
     1.2 +++ b/src/Pure/thm.ML	Sun Sep 28 12:42:35 2008 +0200
     1.3 @@ -1611,7 +1611,7 @@
     1.4  fun join_futures thy =
     1.5    let
     1.6      val futures = Futures.get thy;
     1.7 -    val results = Future.join_results (! futures);
     1.8 +    val results = Future.join_results (rev (! futures));
     1.9      val done = CRITICAL (fn () =>
    1.10        (change futures (filter_out Future.is_finished); null (! futures)));
    1.11      val _ = Future.release_results results;
    1.12 @@ -1662,7 +1662,7 @@
    1.13  
    1.14  fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
    1.15    let
    1.16 -    val _ = Future.release_results (Future.join_results (map #2 promises));
    1.17 +    val _ = Future.release_results (Future.join_results (rev (map #2 promises)));
    1.18      val results = map (apsnd Future.join) promises;
    1.19      val proofs = fold (fn (i, Thm (Deriv {proof = prf, ...}, _)) => Inttab.update (i, prf))
    1.20        results Inttab.empty;