src/Pure/Concurrent/par_list.ML
changeset 32094 89b9210c7506
parent 29368 503ce3f8f092
child 32103 ebdcff2b9810
     1.1 --- a/src/Pure/Concurrent/par_list.ML	Tue Jul 21 10:23:16 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/par_list.ML	Tue Jul 21 10:24:57 2009 +0200
     1.3 @@ -28,11 +28,8 @@
     1.4  
     1.5  fun raw_map f xs =
     1.6    if Future.enabled () then
     1.7 -    let
     1.8 -      val group = Task_Queue.new_group ();
     1.9 -      val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
    1.10 -      val _ = List.app (ignore o Future.join_result) futures;
    1.11 -    in Future.join_results futures end
    1.12 +    let val group = Task_Queue.new_group ()
    1.13 +    in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
    1.14    else map (Exn.capture f) xs;
    1.15  
    1.16  fun map f xs = Exn.release_first (raw_map f xs);