IntGraph.del_node;

--- a/src/Pure/Concurrent/task_queue.ML	Tue Sep 23 15:48:53 2008 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Sep 23 15:48:54 2008 +0200
@@ -156,7 +156,7 @@
   let
     val Group (gid, _) = get_group jobs task;
     val groups' = Inttab.remove_list (op =) (gid, task) groups;
-    val jobs' = IntGraph.del_nodes [id] jobs;
+    val jobs' = IntGraph.del_node id jobs;
     val focus' = remove (op =) task focus;
   in make_queue groups' jobs' focus' end;