| changeset 54734 | b91afc3aa3e6 |
| parent 54732 | b01bb3d09928 |
| child 55033 | 8e8243975860 |
--- a/src/Pure/General/symbol.ML Thu Dec 12 23:18:47 2013 +0100 +++ b/src/Pure/General/symbol.ML Fri Dec 13 12:31:45 2013 +0100 @@ -424,8 +424,7 @@ val scan_encoded_newline = $$ "\^M" -- $$ "\n" >> K "\n" || - $$ "\^M" >> K "\n" || - Scan.this_string "\\<^newline>" >> K "\n"; (*Proof General legacy*) + $$ "\^M" >> K "\n"; val scan_raw = Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||