diff -r 0241916a5f06 -r 3e48bf962e05 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Tue Jul 28 14:29:25 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Jul 28 14:35:27 2009 +0200
@@ -26,8 +26,8 @@
   val cancel_all: queue -> group list
   val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
-  val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
-  val dequeue_towards: task list -> queue ->
+  val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
+  val dequeue_towards: Thread.thread -> task list -> queue ->
     (((task * group * (bool -> bool) list) option * task list) * queue)
   val finish: task -> queue -> bool * queue
 end;
@@ -179,7 +179,7 @@
 
 (* dequeue *)
 
-fun dequeue (queue as Queue {groups, jobs, cache}) =
+fun dequeue thread (queue as Queue {groups, jobs, cache}) =
   let
     fun ready (task, ((group, Job list), ([], _))) = SOME (task, group, rev list)
       | ready _ = NONE;
@@ -188,7 +188,7 @@
         NONE => (NONE, make_queue groups jobs No_Result)
       | SOME (result as (task, _, _)) =>
           let
-            val jobs' = set_job task (Running (Thread.self ())) jobs;
+            val jobs' = set_job task (Running thread) jobs;
             val cache' = Result task;
           in (SOME result, make_queue groups jobs' cache') end);
   in
@@ -201,7 +201,7 @@
 
 (* dequeue_towards -- adhoc dependencies *)
 
-fun dequeue_towards deps (queue as Queue {groups, jobs, ...}) =
+fun dequeue_towards thread deps (queue as Queue {groups, jobs, ...}) =
   let
     fun ready task =
       (case Task_Graph.get_node jobs task of
@@ -213,7 +213,7 @@
     val tasks = filter (can (Task_Graph.get_node jobs)) deps;
     fun result (res as (task, _, _)) =
       let
-        val jobs' = set_job task (Running (Thread.self ())) jobs;
+        val jobs' = set_job task (Running thread) jobs;
         val cache' = Unknown;
       in ((SOME res, tasks), make_queue groups jobs' cache') end;
   in