diff -r 5e9a1d71f94d -r d5803c3d537a src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Jul 13 10:57:09 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Jul 13 16:42:14 2011 +0200
@@ -318,7 +318,7 @@
       | ready (task :: tasks) rest =
           (case try (Task_Graph.get_entry jobs) task of
             NONE => ready tasks rest
-          | SOME entry =>
+          | SOME (_, entry) =>
               (case ready_job task entry of
                 NONE => ready tasks (task :: rest)
               | some => (some, List.revAppend (rest, tasks))));
@@ -327,7 +327,7 @@
       | ready_dep seen (task :: tasks) =
           if Tasks.defined seen task then ready_dep seen tasks
           else
-            let val entry as (_, (ds, _)) = Task_Graph.get_entry jobs task in
+            let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
               (case ready_job task entry of
                 NONE => ready_dep (Tasks.update (task, ()) seen) (ds @ tasks)
               | some => some)