# HG changeset patch
# User wenzelm
# Date 878307620 -3600
# Node ID c88d0d5ae806cca0d54fb46ef7a8c81288acbdd3
# Parent  026069ba0316e74ade8e0ec6cdb9313c53eb370d
added mixfix_args;

diff -r 026069ba0316 -r c88d0d5ae806 src/Pure/Syntax/mixfix.ML
--- 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 =