# HG changeset patch
# User wenzelm
# Date 1177353850 -7200
# Node ID ce1fe6ca7dbbfcc597b87786885d75e2bf3eed42
# Parent  615e19792c928af135ef3c2fb26e05e6b127122e
added paramify_vars;
infer: replace params uniformly (notably freeze);

diff -r 615e19792c92 -r ce1fe6ca7dbb src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Mon Apr 23 20:44:09 2007 +0200
+++ b/src/Pure/type_infer.ML	Mon Apr 23 20:44:10 2007 +0200
@@ -12,6 +12,7 @@
   val polymorphicT: typ -> typ
   val constrain: term -> typ -> term
   val param: int -> string * sort -> typ
+  val paramify_vars: typ -> typ
   val paramify_dummies: typ -> int -> typ * int
   val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
   val infer_types: Pretty.pp -> Type.tsig ->
@@ -41,6 +42,8 @@
 fun is_param_default (x, _) = size x > 0 andalso ord x = ord "?";
 fun param i (x, S) = TVar (("?" ^ x, i), S);
 
+val paramify_vars = Term.map_atyps (fn TVar ((x, i), S) => param i (x, S) | T => T);
+
 val paramify_dummies =
   let
     fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1);
@@ -402,17 +405,16 @@
     val tTs' = ListPair.map Constraint (ts', Ts');
     val _ = List.app (fn t => (infer pp tsig t; ())) tTs';
 
-    (*collect result unifier*)
-    fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE)
-      | ch_var xi_T = SOME xi_T;
-    val env = map_filter ch_var (Vartab.dest Tps);
-
     (*convert back to terms/typs*)
     val mk_var =
       if freeze then PTFree
       else (fn (x, S) => PTVar ((x, 0), S));
     val (final_Ts, final_ts) = typs_terms_of used mk_var "" (Ts', ts');
-    val final_env = map (apsnd simple_typ_of) env;
-  in (final_ts ~~ final_Ts, final_env) end;
+
+    (*collect result unifier*)
+    val redundant = fn (xi, TVar (yi, _)) => xi = yi | _ => false;
+    val env = filter_out redundant (map (apsnd simple_typ_of) (Vartab.dest Tps));
+
+  in (final_ts ~~ final_Ts, env) end;
 
 end;