schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;

--- 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;