diff -r 58f8ff014009 -r 1b37895b607a src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Fri Dec 13 17:38:17 1996 +0100
+++ b/src/Pure/Thy/thy_scan.ML	Fri Dec 13 17:38:56 1996 +0100
@@ -67,6 +67,11 @@
   scan_ctrl || scan_dig ^^ scan_dig ^^ scan_dig ||
   scan_blanks1 ^^ $$ "\\";
 
+fun warn_unprintable c n =
+  (if not (is_printable c) then
+    warning ("Unprintable char \"\\" ^ string_of_int (ord c) ^
+      "\" in string at line " ^ string_of_int n)
+  else (); c);
 
 fun string ("\"" :: cs) n = (["\""], cs, n)
   | string ("\\" :: cs) n =
@@ -76,7 +81,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 cons_fst c (string cs n)
+      else cons_fst (warn_unprintable c n) (string cs n)
   | string [] n = lex_err n "missing quote at end of string";