Symbol.space;
authorwenzelm
Tue, 17 Nov 1998 14:09:29 +0100
changeset 5910 151ee1a5c09c
parent 5909 3fc6497f1c7b
child 5911 7da8033264fa
Symbol.space;
src/Pure/Thy/thy_scan.ML
--- 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 =