1.1 --- a/src/Pure/Concurrent/task_queue.ML	Thu Jul 09 17:34:59 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Thu Jul 09 22:01:41 2009 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  fun str_of_task (Task (_, i)) = string_of_int i;
     1.5  
     1.6  fun task_ord (Task t1, Task t2) = prod_ord (rev_order o int_ord) int_ord (t1, t2);
     1.7 -structure Task_Graph = GraphFun(type key = task val ord = task_ord);
     1.8 +structure Task_Graph = Graph(type key = task val ord = task_ord);
     1.9  
    1.10  
    1.11  (* groups *)