--- 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 =