src/Pure/System/session.ML

--- a/src/Pure/System/session.ML	Thu Oct 18 19:12:58 2012 +0200
+++ b/src/Pure/System/session.ML	Thu Oct 18 19:58:30 2012 +0200
@@ -66,15 +66,18 @@
 
 (* 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 ();
-  Goal.finish_futures ();
+  finish_futures ();
   Thy_Info.finish ();
   Present.finish ();
   Keyword.status ();
   Outer_Syntax.check_syntax ();
-  Goal.cancel_futures ();
-  Future.shutdown ();
   Options.reset_default ();
   session_finished := true);