schedule_tasks: alphabetical order for equivalent tasks;
authorwenzelm
Sat Aug 11 17:50:23 2007 +0200 (2007-08-11)
changeset 242294b5306c36bd9
parent 24228 9e2234f2aff1
child 24230 f63bca3e574e
schedule_tasks: alphabetical order for equivalent tasks;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Fri Aug 10 22:31:19 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Aug 11 17:50:23 2007 +0200
     1.3 @@ -333,8 +333,8 @@
     1.4  local
     1.5  
     1.6  fun max_task (name, (Task body, m)) NONE = SOME (name, (body, m))
     1.7 -  | max_task (name, (Task body, m)) (task' as SOME (_, (_, m'))) =
     1.8 -      if m > m' then SOME (name, (body, m)) else task'
     1.9 +  | max_task (name, (Task body, m)) (task' as SOME (name', (_, m'))) =
    1.10 +      if m > m' orelse m = m' andalso name < name' then SOME (name, (body, m)) else task'
    1.11    | max_task _ task' = task';
    1.12  
    1.13  fun next_task G =