diff -r fcbd6c9ee9bb -r 572b92362496 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Mon Jul 27 12:24:27 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Mon Jul 27 13:32:23 2009 +0200
@@ -30,8 +30,6 @@
   val dequeue_towards: task list -> queue ->
     (((task * group * (bool -> bool) list) * task list) option * queue)
   val finish: task -> queue -> bool * queue
-  val interrupt: queue -> task -> unit
-  val interrupt_external: queue -> string -> unit
 end;
 
 structure Task_Queue:> TASK_QUEUE =
@@ -240,20 +238,4 @@
     val cache' = if maximal then cache else Unknown;
   in (maximal, make_queue groups' jobs' cache') end;
 
-
-(* sporadic interrupts *)
-
-fun interrupt (Queue {jobs, ...}) task =
-  (case try (get_job jobs) task of
-    SOME (Running thread) => SimpleThread.interrupt thread
-  | _ => ());
-
-fun interrupt_external (queue as Queue {jobs, ...}) str =
-  (case Int.fromString str of
-    SOME i =>
-      (case Task_Graph.get_first NONE
-          (fn (task as Task (_, j), _) => if i = j then SOME task else NONE) jobs
-        of SOME task => interrupt queue task | NONE => ())
-  | NONE => ());
-
 end;