more explicit Goal.shutdown_futures;

--- a/src/Pure/System/session.ML	Mon Feb 25 13:31:02 2013 +0100
+++ b/src/Pure/System/session.ML	Mon Feb 25 17:47:32 2013 +0100
@@ -67,14 +67,8 @@
 
 (* finish *)
 
-fun finish_futures () =
-  (case map_filter Task_Queue.group_status (Goal.reset_futures ()) of
-    [] => ()
-  | exns => raise Par_Exn.make exns);
-
 fun finish () =
- (Future.shutdown ();
-  finish_futures ();
+ (Goal.shutdown_futures ();
   Thy_Info.finish ();
   Present.finish ();
   Keyword.status ();

--- a/src/Pure/goal.ML	Mon Feb 25 13:31:02 2013 +0100
+++ b/src/Pure/goal.ML	Mon Feb 25 17:47:32 2013 +0100
@@ -28,6 +28,7 @@
   val fork: int -> (unit -> 'a) -> 'a future
   val peek_futures: serial -> unit future list
   val reset_futures: unit -> Future.group list
+  val shutdown_futures: unit -> unit
   val future_enabled_level: int -> bool
   val future_enabled: unit -> bool
   val future_enabled_nested: int -> bool
@@ -178,6 +179,12 @@
   Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
     (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
 
+fun shutdown_futures () =
+  (Future.shutdown ();
+    (case map_filter Task_Queue.group_status (reset_futures ()) of
+      [] => ()
+    | exns => raise Par_Exn.make exns));
+
 end;