src/Pure/Tools/codegen_serializer.ML
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))