# HG changeset patch
# User wenzelm
# Date 1222177734 -7200
# Node ID c33c8ad8de70e3ffa565fb963ce711f48ac3894d
# Parent  33d58fdc177df08ac45b56382bd972ba0c7097b1
IntGraph.del_node;

diff -r 33d58fdc177d -r c33c8ad8de70 src/Pure/Concurrent/task_queue.ML
--- 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;