# HG changeset patch
# User wenzelm
# Date 1008638423 -3600
# Node ID adc39b100e9a12f9bb04dfadabeb80374b96ebe4
# Parent  c32d201d7c0813f994e04187b9eb2654393dd26b
improved mixfix_args;

diff -r c32d201d7c08 -r adc39b100e9a src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Dec 18 02:20:02 2001 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Tue Dec 18 02:20:23 2001 +0100
@@ -88,7 +88,7 @@
       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 ["'"] = []
@@ -118,13 +118,13 @@
   | 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 *)