changeset 23784 | 75e6b9dd5336 |
parent 23715 | ecce78dfdfc5 |
child 23809 | 6104514a1f5f |
--- a/src/Pure/Tools/codegen_serializer.ML Wed Jul 11 12:23:34 2007 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Wed Jul 11 17:47:45 2007 +0200 @@ -139,7 +139,7 @@ fun parse_mixfix prep_arg s = let - val sym_any = Scan.one Symbol.not_eof; + val sym_any = Scan.one Symbol.is_regular; val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat ( ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR)) || ($$ "_" >> K (Arg BR))