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