changeset 40627 | becf5d5187cc |
parent 40531 | 8ede48c93c72 |
child 40958 | 755f8fe7ced9 |
--- a/src/Pure/Isar/token.ML Fri Nov 19 23:48:07 2010 +0100 +++ b/src/Pure/Isar/token.ML Sat Nov 20 00:53:26 2010 +0100 @@ -265,7 +265,7 @@ (* scan symbolic idents *) -val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~"); +val is_sym_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~"); val scan_symid = Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||