# HG changeset patch
# User wenzelm
# Date 1322309412 -3600
# Node ID 65e4eeea09cd35660c37a462459aef26b9d01669
# Parent  20ef9135a9fb3c53fe1bb0e1ecabc782abab6c48
tuned;

diff -r 20ef9135a9fb -r 65e4eeea09cd src/Pure/Concurrent/task_queue.ML
--- 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) =