# HG changeset patch
# User wenzelm
# Date 1224600790 -7200
# Node ID 4889b48919a0165ced60ac1dbc96e0983885700d
# Parent  8068cdc84e7e925c89b1fa574e6747e490e946f3
join results in isolation;

diff -r 8068cdc84e7e -r 4889b48919a0 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Oct 21 16:53:00 2008 +0200
+++ b/src/Pure/thm.ML	Tue Oct 21 16:53:10 2008 +0200
@@ -1627,7 +1627,7 @@
   let
     val futures = Futures.get thy;
     fun joined () =
-     (Future.join_results (rev (! futures));
+     (List.app (ignore o Future.join_result) (rev (! futures));
       CRITICAL (fn () =>
         let
           val (finished, unfinished) = List.partition Future.is_finished (! futures);