author | wenzelm |
Tue, 17 Nov 1998 14:09:29 +0100 | |
changeset 5910 | 151ee1a5c09c |
parent 5909 | 3fc6497f1c7b |
child 5911 | 7da8033264fa |
--- 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 =