# HG changeset patch
# User wenzelm
# Date 1222532285 -7200
# Node ID 0b8237df37bd09b3732c7a34cb106e9e67fdad65
# Parent  0130201cc0e3e37dd9a4da792181b8dee399cac3
Future.release_results;

diff -r 0130201cc0e3 -r 0b8237df37bd src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Sep 27 15:37:01 2008 +0200
+++ b/src/Pure/thm.ML	Sat Sep 27 18:18:05 2008 +0200
@@ -1614,7 +1614,7 @@
     val results = Future.join_results (! futures);
     val done = CRITICAL (fn () =>
       (change futures (filter_out Future.is_finished); null (! futures)));
-    val _ = ParList.release_results results;
+    val _ = Future.release_results results;
   in if done then NONE else SOME thy end;
 
 val _ = Context.>> (Context.map_theory (Futures.init #> Theory.at_end join_futures));
@@ -1661,7 +1661,7 @@
 
 fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
   let
-    val _ = ParList.release_results (Future.join_results (map #2 promises));
+    val _ = Future.release_results (Future.join_results (map #2 promises));
     val results = map (apsnd Future.join) promises;
     val proofs = fold (fn (i, Thm (Deriv {proof = prf, ...}, _)) => Inttab.update (i, prf))
       results Inttab.empty;