src/Pure/thm.ML
changeset 28648 4889b48919a0
parent 28624 d983515e5cdf
child 28675 fb68c0767004
     1.1 --- a/src/Pure/thm.ML	Tue Oct 21 16:53:00 2008 +0200
     1.2 +++ b/src/Pure/thm.ML	Tue Oct 21 16:53:10 2008 +0200
     1.3 @@ -1627,7 +1627,7 @@
     1.4    let
     1.5      val futures = Futures.get thy;
     1.6      fun joined () =
     1.7 -     (Future.join_results (rev (! futures));
     1.8 +     (List.app (ignore o Future.join_result) (rev (! futures));
     1.9        CRITICAL (fn () =>
    1.10          let
    1.11            val (finished, unfinished) = List.partition Future.is_finished (! futures);