src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Tue Dec 20 08:57:03 2016 +0100
+++ b/src/Pure/General/symbol.scala	Tue Dec 20 09:52:01 2016 +0100
@@ -128,16 +128,6 @@
 
   def explode(text: CharSequence): List[Symbol] = iterator(text).toList
 
-  def advance_line_column(pos: (Int, Int), text: CharSequence): (Int, Int) =
-  {
-    var (line, column) = pos
-    for (sym <- iterator(text)) {
-      if (is_newline(sym)) { line += 1; column = 1 }
-      else column += 1
-    }
-    (line, column)
-  }
-
 
   /* decoding offsets */