uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;

--- a/src/Pure/Thy/thy_info.ML	Sat Jul 02 19:08:51 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Jul 02 19:22:06 2011 +0200
@@ -165,8 +165,10 @@
 
 (* scheduling loader tasks *)
 
+type result = theory * unit future * (unit -> unit);
+
 datatype task =
-  Task of string list * (theory list -> (theory * unit future * (unit -> unit))) |
+  Task of string list * (theory list -> result) |
   Finished of theory;
 
 fun task_finished (Task _) = false
@@ -174,15 +176,15 @@
 
 local
 
+fun finish_thy ((thy, present, commit): result) =
+  (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
+
 fun schedule_seq task_graph =
   ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
     (case Graph.get_node task_graph name of
       Task (parents, body) =>
-        let
-          val (thy, present, commit) = body (map (the o Symtab.lookup tab) parents);
-          val _ = Future.join present;
-          val _ = commit ();
-        in Symtab.update (name, thy) tab end
+        let val result = body (map (the o Symtab.lookup tab) parents)
+        in Symtab.update (name, finish_thy result) tab end
     | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
 
 fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
@@ -210,10 +212,8 @@
     val _ =
       tasks |> maps (fn name =>
         let
-          val (thy, present, commit) = Future.join (the (Symtab.lookup futures name));
-          val _ = Global_Theory.join_proofs thy;
-          val _ = Future.join present;
-          val _ = commit ();
+          val result = Future.join (the (Symtab.lookup futures name));
+          val _ = finish_thy result;
         in [] end handle exn => [Exn.Exn exn])
       |> rev |> Exn.release_all;
   in () end) ();