src/Pure/Concurrent/future.ML

--- a/src/Pure/Concurrent/future.ML	Tue Jan 01 13:37:37 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Jan 01 21:55:46 2013 +0100
@@ -203,7 +203,10 @@
         ("workers_active", Markup.print_int active),
         ("workers_waiting", Markup.print_int waiting)] @
         ML_Statistics.get ();
-    in Output.protocol_message (Markup.ML_statistics @ stats) "" end
+    in
+      Output.protocol_message (Markup.ML_statistics @ stats) ""
+        handle Fail msg => warning msg
+    end
   else ();