# HG changeset patch
# User wenzelm
# Date 1248201451 -7200
# Node ID ebdcff2b9810bf2468e1c3c03daed277e045fdec
# Parent  81d03a29980c9f8bbf2479fc23d63cf62439d660
map: subgroup of worker_group;

diff -r 81d03a29980c -r ebdcff2b9810 src/Pure/Concurrent/par_list.ML
--- 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;