src/Pure/Concurrent/par_list.ML
changeset 32103 ebdcff2b9810
parent 32094 89b9210c7506
child 32255 d302f1c9e356
     1.1 --- a/src/Pure/Concurrent/par_list.ML	Tue Jul 21 20:37:31 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/par_list.ML	Tue Jul 21 20:37:31 2009 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  fun raw_map f xs =
     1.6    if Future.enabled () then
     1.7 -    let val group = Task_Queue.new_group ()
     1.8 +    let val group = Task_Queue.new_group (Future.worker_group ())
     1.9      in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
    1.10    else map (Exn.capture f) xs;
    1.11