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