Future.join_result;
authorwenzelm
Tue, 21 Oct 2008 16:52:59 +0200
changeset 286463a8d75c935ce
parent 28645 605a3b1ef6ba
child 28647 8068cdc84e7e
Future.join_result;
src/Pure/Concurrent/par_list.ML
     1.1 --- a/src/Pure/Concurrent/par_list.ML	Tue Oct 21 15:01:18 2008 +0200
     1.2 +++ b/src/Pure/Concurrent/par_list.ML	Tue Oct 21 16:52:59 2008 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4      let
     1.5        val group = TaskQueue.new_group ();
     1.6        val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
     1.7 -      val _ = List.app (ignore o Future.join_results o single) futures;
     1.8 +      val _ = List.app (ignore o Future.join_result) futures;
     1.9      in Future.join_results futures end
    1.10    else map (Exn.capture f) xs;
    1.11