# HG changeset patch
# User wenzelm
# Date 1133560488 -3600
# Node ID 64cb06a0bb50e7c0b1d1e900f755ea296dc394ec
# Parent  ed2d0e60fbcc9b3ca0c67a0c8790a1da64c46ac7
added mixfixT;
paramify_dummies: treat dummyT as well, tuned;

diff -r ed2d0e60fbcc -r 64cb06a0bb50 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Dec 02 22:54:47 2005 +0100
+++ b/src/Pure/type_infer.ML	Fri Dec 02 22:54:48 2005 +0100
@@ -9,11 +9,12 @@
 sig
   val anyT: sort -> typ
   val logicT: typ
+  val mixfixT: Syntax.mixfix -> typ
   val polymorphicT: typ -> typ
   val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
   val constrain: term -> typ -> term
   val param: int -> string * sort -> typ
-  val paramify_dummies: int * typ -> int * typ
+  val paramify_dummies: typ -> int -> typ * int
   val get_sort: Type.tsig -> (indexname -> sort option) -> (sort -> sort)
     -> (indexname * sort) list -> indexname -> sort
   val infer_types: Pretty.pp
@@ -105,6 +106,10 @@
 fun anyT S = TFree ("'_dummy_", S);
 val logicT = anyT [];
 
+fun mixfixT (Binder _) = (logicT --> logicT) --> logicT
+  | mixfixT mx = replicate (Syntax.mixfix_args mx) logicT ---> logicT;
+
+
 (*indicate polymorphic Vars*)
 fun polymorphicT T = Type ("_polymorphic_", [T]);
 
@@ -436,12 +441,17 @@
 fun is_param (x, _) = size x > 0 andalso ord x = ord "?";
 fun param i (x, S) = TVar (("?" ^ x, i), S);
 
-fun paramify_dummies (maxidx, TFree ("'_dummy_", S)) =
-      (maxidx + 1, param (maxidx + 1) ("'dummy", S))
-  | paramify_dummies (maxidx, Type (a, Ts)) =
-      let val (maxidx', Ts') = foldl_map paramify_dummies (maxidx, Ts)
-      in (maxidx', Type (a, Ts')) end
-  | paramify_dummies arg = arg;
+val paramify_dummies =
+  let
+    fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1);
+
+    fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx
+      | paramify (Type ("dummy", _)) maxidx = dummy [] maxidx
+      | paramify (Type (a, Ts)) maxidx =
+          let val (Ts', maxidx') = fold_map paramify Ts maxidx
+          in (Type (a, Ts'), maxidx') end
+      | paramify T maxidx = (T, maxidx);
+  in paramify end;
 
 
 (* decode sort constraints *)