# HG changeset patch
# User wenzelm
# Date 1191094789 -7200
# Node ID 4c2b872f8cf6215a0f3bd55ff7dab1da85ff378c
# Parent  da4a9986eccd246b0e5829361ba112c190d22afb
added fixate_params;
type_infer: freeze_mode = NONE keeps inference parameters in result;
type_infer: observe Variable.maxidx_of;

diff -r da4a9986eccd -r 4c2b872f8cf6 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Sat Sep 29 21:39:48 2007 +0200
+++ b/src/Pure/type_infer.ML	Sat Sep 29 21:39:49 2007 +0200
@@ -14,10 +14,11 @@
   val param: int -> string * sort -> typ
   val paramify_vars: typ -> typ
   val paramify_dummies: typ -> int -> typ * int
+  val fixate_params: Name.context -> term list -> term list
   val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
   val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
-    (string -> typ option) -> (indexname -> typ option) ->
-    Name.context -> bool -> (term * typ) list -> (term * typ) list * (indexname * typ) list
+    (string -> typ option) -> (indexname -> typ option) -> Name.context -> int -> bool option ->
+    (term * typ) list -> (term * typ) list * (indexname * typ) list
 end;
 
 structure TypeInfer: TYPE_INFER =
@@ -55,6 +56,19 @@
       | paramify T maxidx = (T, maxidx);
   in paramify end;
 
+fun fixate_params name_context ts =
+  let
+    fun subst_param (xi, S) (inst, used) =
+      if is_param xi then
+        let
+          val [a] = Name.invents used "'a" 1;
+          val used' = Name.declare a used;
+        in (((xi, S), TFree (a, S)) :: inst, used') end
+      else (inst, used);
+    val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
+    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
+  in (map o map_types) (TermSubst.instantiateT inst) ts end;
+
 
 
 (** pretyps and preterms **)
@@ -380,7 +394,7 @@
 
 (* infer_types *)
 
-fun infer_types pp tsig check_typs const_type var_type used freeze args =
+fun infer_types pp tsig check_typs const_type var_type used maxidx freeze_mode args =
   let
     (*check types*)
     val (raw_ts, raw_Ts) = split_list args;
@@ -405,9 +419,10 @@
 
     (*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');
+      if the_default false freeze_mode then PTFree
+      else (fn (x, S) => PTVar ((x, maxidx + 1), S));
+    val prfx = if is_some freeze_mode then "" else "?";
+    val (final_Ts, final_ts) = typs_terms_of used mk_var prfx (Ts', ts');
 
     (*collect result unifier*)
     val redundant = fn (xi, TVar (yi, _)) => xi = yi | _ => false;