author | wenzelm |
Fri, 08 Aug 2008 13:36:44 +0200 | |
changeset 27791 | 23d2567c578e |
parent 27790 | 37b4e65d1dbf |
child 27792 | e4a4d057749d |
--- 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);