tuned;

--- a/src/Pure/Concurrent/task_queue.ML	Fri Nov 25 23:04:12 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Nov 26 13:10:12 2011 +0100
@@ -340,7 +340,7 @@
           | SOME (_, entry) =>
               (case ready_job task entry of
                 NONE => ready tasks (task :: rest)
-              | some => (some, List.revAppend (rest, tasks))));
+              | some => (some, fold cons rest tasks)));
 
     fun ready_dep _ [] = NONE
       | ready_dep seen (task :: tasks) =