changeset 978 | f7011b47ac38 |
parent 712 | 1f5800d2c366 |
child 1512 | ce37c64244c0 |
--- a/src/Pure/Thy/thy_scan.ML Tue Mar 28 12:25:20 1995 +0200 +++ b/src/Pure/Thy/thy_scan.ML Tue Mar 28 13:13:17 1995 +0200 @@ -74,8 +74,7 @@ (None, _) => lex_err n "bad escape sequence in string" | (Some s, cs') => cons_fst ("\\" ^ s) (string cs' (inc_line n s))) | string (c :: cs) n = - if c = "\n" then - lex_err n "no matching quote found on this line" + if c = "\n" then string cs (n+1) else cons_fst c (string cs n) | string [] n = lex_err n "missing quote at end of string";