1.1 --- a/src/Pure/Concurrent/task_queue.ML	Wed Sep 10 22:29:36 2008 +0200
     1.2 +++ b/src/Pure/Concurrent/task_queue.ML	Wed Sep 10 23:19:36 2008 +0200
     1.3 @@ -8,9 +8,9 @@
     1.4  signature TASK_QUEUE =
     1.5  sig
     1.6    eqtype task
     1.7 +  val str_of_task: task -> string
     1.8    eqtype group
     1.9    val new_group: unit -> group
    1.10 -  val str_of_task: task -> string
    1.11    val str_of_group: group -> string
    1.12    type queue
    1.13    val empty: queue
    1.14 @@ -116,7 +116,7 @@
    1.15  
    1.16  (* termination *)
    1.17  
    1.18 -fun cancel (Queue {groups, jobs}) (group as Group (gid, ok)) =
    1.19 +fun cancel (Queue {groups, jobs}) (Group (gid, ok)) =
    1.20    let
    1.21      val _ = ok := false;  (*invalidate any future group members*)
    1.22      val tasks = Inttab.lookup_list groups gid;