src/Pure/Thy/thy_scan.ML
changeset 5910 151ee1a5c09c
parent 5112 9e74cf11e4a4
child 6207 58e9f980bd4f
--- a/src/Pure/Thy/thy_scan.ML	Tue Nov 17 14:09:00 1998 +0100
+++ b/src/Pure/Thy/thy_scan.ML	Tue Nov 17 14:09:29 1998 +0100
@@ -73,7 +73,7 @@
 
 val scan_str =
   scan_esc ||
-  scan_blank >> K " " ||
+  scan_blank >> K Symbol.space ||
   keep_line (Scan.one (not_equal "\"" andf Symbol.not_eof));
 
 val scan_string =