--- a/src/Pure/Concurrent/par_list.ML Tue Jul 21 10:23:16 2009 +0200
+++ b/src/Pure/Concurrent/par_list.ML Tue Jul 21 10:24:57 2009 +0200
@@ -28,11 +28,8 @@
fun raw_map f xs =
if Future.enabled () then
- let
- val group = Task_Queue.new_group ();
- val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
- val _ = List.app (ignore o Future.join_result) futures;
- in Future.join_results futures end
+ let val group = Task_Queue.new_group ()
+ in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
else map (Exn.capture f) xs;
fun map f xs = Exn.release_first (raw_map f xs);