author | wenzelm |
Sun, 12 Aug 2007 14:14:24 +0200 | |
changeset 24230 | f63bca3e574e |
parent 24229 | 4b5306c36bd9 |
child 24231 | 85fb973a8207 |
--- a/src/Pure/Thy/thy_info.ML Sat Aug 11 17:50:23 2007 +0200 +++ b/src/Pure/Thy/thy_info.ML Sun Aug 12 14:14:24 2007 +0200 @@ -332,7 +332,7 @@ local -fun max_task (name, (Task body, m)) NONE = SOME (name, (body, m)) +fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m)) | 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';