src/Pure/Concurrent/par_list.ML
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