changeset 2338 | 1871df9900bf |
parent 2204 | 64cb98f841e4 |
child 2387 | 1b37895b607a |
--- a/src/Pure/Thy/thy_scan.ML Mon Dec 09 10:01:04 1996 +0100 +++ b/src/Pure/Thy/thy_scan.ML Mon Dec 09 15:14:08 1996 +0100 @@ -76,8 +76,7 @@ | string ("\n" :: cs) n = cons_fst " " (string cs (n + 1)) | string (c :: cs) n = if is_blank c then cons_fst " " (string cs n) - else if is_printable c then cons_fst c (string cs n) - else cons_fst ("\\" ^ string_of_int (ord c)) (string cs n) + else cons_fst c (string cs n) | string [] n = lex_err n "missing quote at end of string";