--- a/src/Pure/Concurrent/par_list.ML Tue Jul 20 23:16:21 2010 +0200
+++ b/src/Pure/Concurrent/par_list.ML Wed Jul 21 13:25:14 2010 +0200
@@ -28,8 +28,8 @@
fun raw_map f xs =
if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then
- 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
+ let val shared_group = Task_Queue.new_group (Future.worker_group ())
+ in Future.join_results (map (fn x => Future.fork_group shared_group (fn () => f x)) xs) end
else map (Exn.capture f) xs;
fun map f xs = Exn.release_first (raw_map f xs);