# HG changeset patch
# User wenzelm
# Date 1222598555 -7200
# Node ID 1a4804fc2216a4643c9958e5d59424a649bb395e
# Parent  0b9fb63b8e1d6511893dd893a7ac8cfc88576df5
join earlier promises first;

diff -r 0b9fb63b8e1d -r 1a4804fc2216 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Sep 28 12:23:45 2008 +0200
+++ b/src/Pure/thm.ML	Sun Sep 28 12:42:35 2008 +0200
@@ -1611,7 +1611,7 @@
 fun join_futures thy =
   let
     val futures = Futures.get thy;
-    val results = Future.join_results (! futures);
+    val results = Future.join_results (rev (! futures));
     val done = CRITICAL (fn () =>
       (change futures (filter_out Future.is_finished); null (! futures)));
     val _ = Future.release_results results;
@@ -1662,7 +1662,7 @@
 
 fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
   let
-    val _ = Future.release_results (Future.join_results (map #2 promises));
+    val _ = Future.release_results (Future.join_results (rev (map #2 promises)));
     val results = map (apsnd Future.join) promises;
     val proofs = fold (fn (i, Thm (Deriv {proof = prf, ...}, _)) => Inttab.update (i, prf))
       results Inttab.empty;