src/Pure/Syntax/mixfix.ML

   | string_of_mixfix (Infixr p) = parens (spaces ["infixr", string_of_int p])
   | string_of_mixfix (Binder (sy, p1, p2)) =
       parens (spaces ["binder", brackets (string_of_int p1), string_of_int p2]);
 
 
-(* type / const names *)
+(* syntax specifications *)
 
 fun strip ("'" :: c :: cs) = c :: strip cs
   | strip ["'"] = []
   | strip (c :: cs) = c :: strip cs
   | strip [] = [];

 fun fix_mixfix c (Infix p) = (InfixName (c, p))
   | fix_mixfix c (Infixl p) = (InfixlName (c, p))
   | fix_mixfix c (Infixr p) = (InfixrName (c, p))
   | fix_mixfix _ mx = mx;
 
-
-(* mixfix_args *)
-
 fun mixfix_args NoSyn = 0
   | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
   | mixfix_args (Delimfix sy) = SynExt.mfix_args sy
-  | mixfix_args (*infix or binder*) _ = 2;
+  | mixfix_args (InfixName (sy, _)) = 2 + SynExt.mfix_args sy
+  | mixfix_args (InfixlName (sy, _)) = 2 + SynExt.mfix_args sy
+  | mixfix_args (InfixrName (sy, _)) = 2 + SynExt.mfix_args sy
+  | mixfix_args (*old infix or binder*) _ = 2;
 
 
 (* syn_ext_types *)
 
 fun syn_ext_types logtypes type_decls =