diff -r 92fa590bdfe0 -r b91afc3aa3e6 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Dec 12 23:18:47 2013 +0100
+++ b/src/Pure/General/symbol.scala	Fri Dec 13 12:31:45 2013 +0100
@@ -51,7 +51,7 @@
       case _ => !s.endsWith(">") || s == "\\<>" || s == "\\<^>"
     }
 
-  def is_physical_newline(s: Symbol): Boolean =
+  def is_newline(s: Symbol): Boolean =
     s == "\n" || s == "\r" || s == "\r\n"
 
   class Matcher(text: CharSequence)
@@ -102,7 +102,7 @@
   {
     var (line, column) = pos
     for (sym <- iterator(text)) {
-      if (is_physical_newline(sym)) { line += 1; column = 1 }
+      if (is_newline(sym)) { line += 1; column = 1 }
       else column += 1
     }
     (line, column)
@@ -358,7 +358,7 @@
       "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
       "\\<Psi>", "\\<Omega>")
 
-    val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<^newline>")
+    val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n")
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")