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