# HG changeset patch
# User wenzelm
# Date 1176640322 -7200
# Node ID 372da033ed93f71af91953f2641d5d5910ad3eb0
# Parent  4346f230283d0fbbc44e976186cbab01ced13180
added mixfixT (from type_infer.ML);

diff -r 4346f230283d -r 372da033ed93 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Sun Apr 15 14:32:01 2007 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sun Apr 15 14:32:02 2007 +0200
@@ -33,6 +33,7 @@
   val const_mixfix: string -> mixfix -> string * mixfix
   val unlocalize_mixfix: mixfix -> mixfix
   val mixfix_args: mixfix -> int
+  val mixfixT: mixfix -> typ
 end;
 
 signature MIXFIX =
@@ -153,6 +154,9 @@
   | mixfix_args (Binder _) = 1
   | mixfix_args Structure = 0;
 
+fun mixfixT (Binder _) = (TypeInfer.logicT --> TypeInfer.logicT) --> TypeInfer.logicT
+  | mixfixT mx = replicate (mixfix_args mx) TypeInfer.logicT ---> TypeInfer.logicT;
+
 
 (* syn_ext_types *)