--- a/src/Pure/ML/ml_lex.ML Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Fri Oct 31 22:02:49 2014 +0100
@@ -236,7 +236,7 @@
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);
val scan_str =
- Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso
+ Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso
(not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single ||
$$$ "\\" @@@ !!! "bad escape character in string" scan_escape;