changeset 45642 | 65e4eeea09cd |
parent 45354 | a2157057024c |
child 47404 | e6e5750f1311 |
--- 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) =