src/Pure/thm.ML
changeset 28648 4889b48919a0
parent 28624 d983515e5cdf
child 28675 fb68c0767004
equal deleted inserted replaced
28647:8068cdc84e7e 28648:4889b48919a0
  1625 
  1625 
  1626 fun join_futures thy =
  1626 fun join_futures thy =
  1627   let
  1627   let
  1628     val futures = Futures.get thy;
  1628     val futures = Futures.get thy;
  1629     fun joined () =
  1629     fun joined () =
  1630      (Future.join_results (rev (! futures));
  1630      (List.app (ignore o Future.join_result) (rev (! futures));
  1631       CRITICAL (fn () =>
  1631       CRITICAL (fn () =>
  1632         let
  1632         let
  1633           val (finished, unfinished) = List.partition Future.is_finished (! futures);
  1633           val (finished, unfinished) = List.partition Future.is_finished (! futures);
  1634           val _ = futures := unfinished;
  1634           val _ = futures := unfinished;
  1635         in finished end)
  1635         in finished end)