added mixfix_args;

--- a/src/Pure/Syntax/mixfix.ML	Fri Oct 31 15:19:50 1997 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Oct 31 15:20:20 1997 +0100
@@ -17,6 +17,7 @@
     Infixr of int |
     Binder of string * int * int
   val max_pri: int
+  val mixfix_args: mixfix -> int
 end;
 
 signature MIXFIX1 =
@@ -82,6 +83,14 @@
   | const_name c _ = c;
 
 
+(* mixfix_args *)
+
+fun mixfix_args NoSyn = 0
+  | mixfix_args (Mixfix (sy, _, _)) = mfix_args sy
+  | mixfix_args (Delimfix sy) = mfix_args sy
+  | mixfix_args _ = 2 		(*infix or binder*);
+
+
 (* syn_ext_types *)
 
 fun syn_ext_types logtypes type_decls =