# HG changeset patch
# User wenzelm
# Date 1186847423 -7200
# Node ID 4b5306c36bd96c5cd2849e0ccbbe795fc730fe7b
# Parent  9e2234f2aff12021168248d313ac760ea46c45b9
schedule_tasks: alphabetical order for equivalent tasks;

diff -r 9e2234f2aff1 -r 4b5306c36bd9 src/Pure/Thy/thy_info.ML
--- 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 =