# HG changeset patch
# User wenzelm
# Date 1238497156 -7200
# Node ID 17bd1cf53d8ef4c583d55bb7cd75af0e74528c08
# Parent  684720b0b9e69f9c5f9daa1f7c5f97431a17aa38
schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;

diff -r 684720b0b9e6 -r 17bd1cf53d8e src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Mar 30 23:12:13 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Mar 31 12:59:16 2009 +0200
@@ -371,7 +371,7 @@
 
     val futures = fold fork tasks Symtab.empty;
 
-    val exns = rev tasks |> maps (fn (name, _) =>
+    val exns = tasks |> maps (fn (name, _) =>
       let
         val after_load = Future.join (the (Symtab.lookup futures name));
         val proof_exns = join_thy name;