schedule_futures: discontinued special treatment of non-parallel proofs, which might have affected memory usage at some point, but does not seem to make a difference with as little as 2GB RAM;

--- a/src/Pure/Thy/thy_info.ML	Tue Aug 03 22:28:43 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Aug 04 14:46:17 2010 +0200
@@ -174,8 +174,6 @@
 fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
   let
     val tasks = Graph.topological_order task_graph;
-    val par_proofs = ! parallel_proofs >= 1;
-
     val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
       (case Graph.get_node task_graph name of
         Task (parents, body) =>
@@ -189,12 +187,8 @@
                 [] => body (map (#1 o Future.join o get) parents)
               | bad => error (loader_msg
                   ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
-            val future' =
-              if par_proofs then future
-              else Future.map (fn (thy, after_load) => (after_load (); (thy, I))) future;
-          in Symtab.update (name, future') tab end
+          in Symtab.update (name, future) tab end
       | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
-
     val _ =
       tasks |> maps (fn name =>
         let