--- a/src/Pure/Thy/thy_info.ML Fri Aug 10 22:31:19 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML Sat Aug 11 17:50:23 2007 +0200
@@ -333,8 +333,8 @@
local
fun max_task (name, (Task body, m)) NONE = SOME (name, (body, m))
- | max_task (name, (Task body, m)) (task' as SOME (_, (_, m'))) =
- if m > m' then SOME (name, (body, m)) else task'
+ | max_task (name, (Task body, m)) (task' as SOME (name', (_, m'))) =
+ if m > m' orelse m = m' andalso name < name' then SOME (name, (body, m)) else task'
| max_task _ task' = task';
fun next_task G =