# HG changeset patch
# User wenzelm
# Date 1218195404 -7200
# Node ID 23d2567c578e9022d33c5acce40032e5bcbd22c3
# Parent  37b4e65d1dbf86d6c54a60f63c6380c7575a07d7
made SML/NJ happy;

diff -r 37b4e65d1dbf -r 23d2567c578e src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Fri Aug 08 09:44:16 2008 +0200
+++ b/src/Pure/General/position.ML	Fri Aug 08 13:36:44 2008 +0200
@@ -46,7 +46,7 @@
 
 (* advance *)
 
-fun advance_count "\n" (m, n) = (m + 1, if valid n then 1 else n)
+fun advance_count "\n" (m: int, n: int) = (m + 1, if valid n then 1 else n)
   | advance_count s (m, n) =
       if valid n andalso Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s)
       then (m, n + 1) else (m, n);