diff -r 30996b775a7f -r 89b9210c7506 src/Pure/Concurrent/par_list.ML
--- 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);