added mixfixT (from type_infer.ML);
authorwenzelm
Sun Apr 15 14:32:02 2007 +0200 (2007-04-15)
changeset 22702372da033ed93
parent 22701 4346f230283d
child 22703 d9fbdfe22543
added mixfixT (from type_infer.ML);
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Sun Apr 15 14:32:01 2007 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Sun Apr 15 14:32:02 2007 +0200
     1.3 @@ -33,6 +33,7 @@
     1.4    val const_mixfix: string -> mixfix -> string * mixfix
     1.5    val unlocalize_mixfix: mixfix -> mixfix
     1.6    val mixfix_args: mixfix -> int
     1.7 +  val mixfixT: mixfix -> typ
     1.8  end;
     1.9  
    1.10  signature MIXFIX =
    1.11 @@ -153,6 +154,9 @@
    1.12    | mixfix_args (Binder _) = 1
    1.13    | mixfix_args Structure = 0;
    1.14  
    1.15 +fun mixfixT (Binder _) = (TypeInfer.logicT --> TypeInfer.logicT) --> TypeInfer.logicT
    1.16 +  | mixfixT mx = replicate (mixfix_args mx) TypeInfer.logicT ---> TypeInfer.logicT;
    1.17 +
    1.18  
    1.19  (* syn_ext_types *)
    1.20