# HG changeset patch
# User wenzelm
# Date 1186920864 -7200
# Node ID f63bca3e574e2b9a01a06b6ace9c142e0ed0e8b0
# Parent  4b5306c36bd96c5cd2849e0ccbbe795fc730fe7b
made SML/NJ happy;

diff -r 4b5306c36bd9 -r f63bca3e574e src/Pure/Thy/thy_info.ML
--- 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';