# HG changeset patch
# User wenzelm
# Date 1221159849 -7200
# Node ID 17a81e48114289583b0b5243fa0b05fe378300cd
# Parent  2d93b158ad99e54b831635c35b4fd7f0ce047e58
finish: Future.shutdown;

diff -r 2d93b158ad99 -r 17a81e481142 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Thu Sep 11 21:04:07 2008 +0200
+++ b/src/Pure/Isar/session.ML	Thu Sep 11 21:04:09 2008 +0200
@@ -68,6 +68,7 @@
 fun finish () =
   (Output.accumulated_time ();
     ThyInfo.finish ();
+    Future.shutdown ();
     Present.finish ();
     session_finished := true);