author | wenzelm |
Tue, 21 Jul 2009 20:37:31 +0200 | |
changeset 32103 | ebdcff2b9810 |
parent 32102 | 81d03a29980c |
child 32104 | d1d98a02473e |
--- a/src/Pure/Concurrent/par_list.ML Tue Jul 21 20:37:31 2009 +0200 +++ b/src/Pure/Concurrent/par_list.ML Tue Jul 21 20:37:31 2009 +0200 @@ -28,7 +28,7 @@ fun raw_map f xs = if Future.enabled () then - let val group = Task_Queue.new_group () + let val group = Task_Queue.new_group (Future.worker_group ()) in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end else map (Exn.capture f) xs;