made SML/NJ happy;
authorwenzelm
Sun Aug 12 14:14:24 2007 +0200 (2007-08-12)
changeset 24230f63bca3e574e
parent 24229 4b5306c36bd9
child 24231 85fb973a8207
made SML/NJ happy;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Sat Aug 11 17:50:23 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Aug 12 14:14:24 2007 +0200
     1.3 @@ -332,7 +332,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun max_task (name, (Task body, m)) NONE = SOME (name, (body, m))
     1.8 +fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m))
     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';