# HG changeset patch
# User wenzelm
# Date 1221081576 -7200
# Node ID f019dd2db561a2345136eb5b4ffc622ac2ae50e8
# Parent  3eaad200d67a5834e2d36cf89b0931c7557dc909
tuned;

diff -r 3eaad200d67a -r f019dd2db561 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Sep 10 22:29:36 2008 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Sep 10 23:19:36 2008 +0200
@@ -8,9 +8,9 @@
 signature TASK_QUEUE =
 sig
   eqtype task
+  val str_of_task: task -> string
   eqtype group
   val new_group: unit -> group
-  val str_of_task: task -> string
   val str_of_group: group -> string
   type queue
   val empty: queue
@@ -116,7 +116,7 @@
 
 (* termination *)
 
-fun cancel (Queue {groups, jobs}) (group as Group (gid, ok)) =
+fun cancel (Queue {groups, jobs}) (Group (gid, ok)) =
   let
     val _ = ok := false;  (*invalidate any future group members*)
     val tasks = Inttab.lookup_list groups gid;