# HG changeset patch
# User wenzelm
# Date 850140848 -3600
# Node ID 1871df9900bfcfa80bfbd9210df68b3549c28e0a
# Parent  5b18cc02adb79e30b78149b11de53d0c691e82e7
removed escaping of 8bit chars;

diff -r 5b18cc02adb7 -r 1871df9900bf src/Pure/Thy/thy_scan.ML
--- 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";