| changeset 27759 | ffb1b5f2690f |
| parent 27749 | 24f2b57a34ea |
| child 27764 | e0ee3cc240fe |
--- a/src/Pure/General/position.ML Wed Aug 06 00:58:27 2008 +0200 +++ b/src/Pure/General/position.ML Wed Aug 06 10:43:42 2008 +0200 @@ -55,7 +55,7 @@ (* advance position *) -fun advance_count "\n" (m, _) = (m + 1, 1) +fun advance_count "\n" (m: int, _: int) = (m + 1, 1) | advance_count s (m, n) = if Symbol.is_regular s andalso not (Symbol.is_utf8_trailer s) then (m, n + 1) else (m, n);