merged

--- a/src/Pure/Thy/thy_info.ML	Sun Jan 11 14:18:32 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sun Jan 11 14:22:34 2009 +0100
@@ -350,6 +350,8 @@
     val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
       (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
 
+    val par_proofs = ! parallel_proofs;
+
     fun fork (name, body) tab =
       let
         val deps = Graph.imm_preds task_graph name
@@ -357,12 +359,15 @@
             (case Symtab.lookup tab parent of SOME future => SOME (parent, future) | NONE => NONE));
         fun failed (parent, future) = if can Future.join future then NONE else SOME parent;
 
-        val x = Future.fork_deps (map #2 deps) (fn () =>
+        val future = Future.fork_deps (map #2 deps) (fn () =>
           (case map_filter failed deps of
             [] => body ()
           | bad => error (loader_msg
               ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
-      in Symtab.update (name, x) tab end;
+        val future' =
+          if par_proofs then future
+          else Future.map (fn after_load => (after_load (); fn () => ())) future;
+      in Symtab.update (name, future') tab end;
 
     val futures = fold fork tasks Symtab.empty;
 

--- a/src/Pure/thm.ML	Sun Jan 11 14:18:32 2009 +0100
+++ b/src/Pure/thm.ML	Sun Jan 11 14:22:34 2009 +0100
@@ -1613,7 +1613,7 @@
     val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
 
     val i = serial ();
-    val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof);
+    val future = future_thm |> Future.map (future_result i thy sorts prop);
     val promise = (i, future);
   in
     Thm (make_deriv i [promise] [promise] [] [] (Pt.promise_proof thy i prop),