changeset 29120 | 8a904ff43f28 |
parent 28980 | 9d7ea903e877 |
child 29368 | 503ce3f8f092 |
--- a/src/Pure/Concurrent/par_list.ML Tue Dec 16 16:25:18 2008 +0100 +++ b/src/Pure/Concurrent/par_list.ML Tue Dec 16 16:25:19 2008 +0100 @@ -30,7 +30,7 @@ fun raw_map f xs = if Future.enabled () then let - val group = TaskQueue.new_group (); + val group = Task_Queue.new_group (); val futures = map (fn x => Future.fork_group group (fn () => f x)) xs; val _ = List.app (ignore o Future.join_result) futures; in Future.join_results futures end