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);