# HG changeset patch
# User wenzelm
# Date 1218012222 -7200
# Node ID ffb1b5f2690f0b4872b2724e5cff2c1d9031dbf7
# Parent  c1e60d8cba07387e04668618315c7b1f0ad1bd88
made SML/NJ happy;

diff -r c1e60d8cba07 -r ffb1b5f2690f src/Pure/General/position.ML
--- 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);