added mixfix_args;
authorwenzelm
Fri Oct 31 15:20:20 1997 +0100 (1997-10-31)
changeset 4053c88d0d5ae806
parent 4052 026069ba0316
child 4054 b33e02b3478e
added mixfix_args;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Oct 31 15:19:50 1997 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Oct 31 15:20:20 1997 +0100
     1.3 @@ -17,6 +17,7 @@
     1.4      Infixr of int |
     1.5      Binder of string * int * int
     1.6    val max_pri: int
     1.7 +  val mixfix_args: mixfix -> int
     1.8  end;
     1.9  
    1.10  signature MIXFIX1 =
    1.11 @@ -82,6 +83,14 @@
    1.12    | const_name c _ = c;
    1.13  
    1.14  
    1.15 +(* mixfix_args *)
    1.16 +
    1.17 +fun mixfix_args NoSyn = 0
    1.18 +  | mixfix_args (Mixfix (sy, _, _)) = mfix_args sy
    1.19 +  | mixfix_args (Delimfix sy) = mfix_args sy
    1.20 +  | mixfix_args _ = 2 		(*infix or binder*);
    1.21 +
    1.22 +
    1.23  (* syn_ext_types *)
    1.24  
    1.25  fun syn_ext_types logtypes type_decls =