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 *)