--- a/src/Pure/Syntax/syntax_ext.ML Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML Fri Oct 31 22:02:49 2014 +0100
@@ -143,8 +143,8 @@
val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
val scan_delim_char =
- $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) ||
- Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular);
+ $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
+ Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
fun read_int ["0", "0"] = ~1
| read_int cs = #1 (Library.read_int cs);