src/Pure/thm.ML
changeset 28381 0b8237df37bd
parent 28378 60cc0359363d
child 28389 777bdc429ea3
     1.1 --- a/src/Pure/thm.ML	Sat Sep 27 15:37:01 2008 +0200
     1.2 +++ b/src/Pure/thm.ML	Sat Sep 27 18:18:05 2008 +0200
     1.3 @@ -1614,7 +1614,7 @@
     1.4      val results = Future.join_results (! futures);
     1.5      val done = CRITICAL (fn () =>
     1.6        (change futures (filter_out Future.is_finished); null (! futures)));
     1.7 -    val _ = ParList.release_results results;
     1.8 +    val _ = Future.release_results results;
     1.9    in if done then NONE else SOME thy end;
    1.10  
    1.11  val _ = Context.>> (Context.map_theory (Futures.init #> Theory.at_end join_futures));
    1.12 @@ -1661,7 +1661,7 @@
    1.13  
    1.14  fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
    1.15    let
    1.16 -    val _ = ParList.release_results (Future.join_results (map #2 promises));
    1.17 +    val _ = Future.release_results (Future.join_results (map #2 promises));
    1.18      val results = map (apsnd Future.join) promises;
    1.19      val proofs = fold (fn (i, Thm (Deriv {proof = prf, ...}, _)) => Inttab.update (i, prf))
    1.20        results Inttab.empty;