# HG changeset patch
# User wenzelm
# Date 1229441119 -3600
# Node ID 8a904ff43f2894a8e0ff58d90affdd034ba4365b
# Parent  99941fd0cb0e70f62a3774279eb59152b604b2f2
renamed structure TaskQueue to Task_Queue;

diff -r 99941fd0cb0e -r 8a904ff43f28 src/Pure/Concurrent/par_list.ML
--- 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