Changed treatment of during type inference internally generated type
authornipkow
Mon Mar 13 09:38:10 1995 +0100 (1995-03-13)
changeset 94983c588d6fee9
parent 948 3647161d15d3
child 950 323f8ca4587a
Changed treatment of during type inference internally generated type
variables.

1. They are renamed to 'a, 'b, 'c etc away from a given set of used names.
2. They are either frozen (turned into TFrees) or left schematic (TVars)
depending on a parameter. In goals they are frozen, for instantiations they
are left schematic.
src/Pure/drule.ML
src/Pure/sign.ML
src/Pure/tactic.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/drule.ML	Sat Mar 11 17:46:14 1995 +0100
     1.2 +++ b/src/Pure/drule.ML	Mon Mar 13 09:38:10 1995 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4    val read_insts	:
     1.5            Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
     1.6                    -> (indexname -> typ option) * (indexname -> sort option)
     1.7 -                  -> (string*string)list
     1.8 +                  -> string list -> (string*string)list
     1.9                    -> (indexname*ctyp)list * (cterm*cterm)list
    1.10    val reflexive_thm	: thm
    1.11    val revcut_rl		: thm
    1.12 @@ -249,7 +249,7 @@
    1.13  fun inst_failure ixn =
    1.14    error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
    1.15  
    1.16 -fun read_insts sign (rtypes,rsorts) (types,sorts) insts =
    1.17 +fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
    1.18  let val {tsig,...} = Sign.rep_sg sign
    1.19      fun split([],tvs,vs) = (tvs,vs)
    1.20        | split((sv,st)::l,tvs,vs) = (case explode sv of
    1.21 @@ -264,14 +264,15 @@
    1.22             else inst_failure ixn
    1.23          end
    1.24      val tye = map readT tvs;
    1.25 -    fun add_cterm ((cts,tye), (ixn,st)) =
    1.26 +    fun add_cterm ((cts,tye,used), (ixn,st)) =
    1.27          let val T = case rtypes ixn of
    1.28                        Some T => typ_subst_TVars tye T
    1.29                      | None => absent ixn;
    1.30 -            val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
    1.31 +            val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T);
    1.32              val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
    1.33 -        in ((cv,ct)::cts,tye2 @ tye) end
    1.34 -    val (cterms,tye') = foldl add_cterm (([],tye), vs);
    1.35 +            val used' = add_term_tvarnames(term_of ct,used);
    1.36 +        in ((cv,ct)::cts,tye2 @ tye,used') end
    1.37 +    val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs);
    1.38  in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
    1.39  
    1.40  
    1.41 @@ -584,7 +585,7 @@
    1.42  (*Instantiate theorem th, reading instantiations under signature sg*)
    1.43  fun read_instantiate_sg sg sinsts th =
    1.44      let val ts = types_sorts th;
    1.45 -    in  instantiate (read_insts sg ts ts sinsts) th  end;
    1.46 +    in  instantiate (read_insts sg ts ts [] sinsts) th  end;
    1.47  
    1.48  (*Instantiate theorem th, reading instantiations under theory of th*)
    1.49  fun read_instantiate sinsts th =
     2.1 --- a/src/Pure/sign.ML	Sat Mar 11 17:46:14 1995 +0100
     2.2 +++ b/src/Pure/sign.ML	Mon Mar 13 09:38:10 1995 +0100
     2.3 @@ -39,8 +39,8 @@
     2.4      val certify_term: sg -> term -> term * typ * int
     2.5      val read_typ: sg * (indexname -> sort option) -> string -> typ
     2.6      val infer_types: sg -> (indexname -> typ option) ->
     2.7 -      (indexname -> sort option) -> bool -> term list * typ ->
     2.8 -      int * term * (indexname * typ) list
     2.9 +      (indexname -> sort option) -> string list -> bool -> bool
    2.10 +      -> term list * typ -> int * term * (indexname * typ) list
    2.11      val add_classes: (class * class list) list -> sg -> sg
    2.12      val add_classrel: (class * class) list -> sg -> sg
    2.13      val add_defsort: sort -> sg -> sg
    2.14 @@ -252,7 +252,7 @@
    2.15  
    2.16  (** infer_types **)         (*exception ERROR*)
    2.17  
    2.18 -fun infer_types sg types sorts print_msg (ts, T) =
    2.19 +fun infer_types sg types sorts used freeze print_msg (ts, T) =
    2.20    let
    2.21      val Sg {tsig, ...} = sg;
    2.22      val show_typ = string_of_typ sg;
    2.23 @@ -268,16 +268,16 @@
    2.24  	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n";
    2.25  
    2.26      val T' = certify_typ sg T
    2.27 -      handle TYPE arg => error (exn_type_msg arg);
    2.28 +             handle TYPE arg => error (exn_type_msg arg);
    2.29  
    2.30      val ct = const_type sg;
    2.31  
    2.32      fun process_terms (t::ts) (idx, infrd_t, tye) msg n =
    2.33 -         let fun mk_some (x, y) = (Some x, Some y);
    2.34 -
    2.35 -             val ((infrd_t', tye'), msg') = 
    2.36 -              (mk_some (Type.infer_types (tsig, ct, types, sorts, T', t)), msg)
    2.37 -              handle TYPE arg => ((None, None), exn_type_msg arg)
    2.38 +         let val (infrd_t', tye', msg') = 
    2.39 +              let val (T,tye) =
    2.40 +                    Type.infer_types(tsig,ct,types,sorts,used,freeze,T',t)
    2.41 +              in (Some T, Some tye, msg) end
    2.42 +              handle TYPE arg => (None, None, exn_type_msg arg)
    2.43  
    2.44               val old_show_brackets = !show_brackets;
    2.45  
    2.46 @@ -291,8 +291,8 @@
    2.47                  (show_term (the infrd_t)) else msg') ^ "\n" ^ 
    2.48                  (show_term (the infrd_t')) ^ "\n";
    2.49  
    2.50 -             val _ = (show_brackets := old_show_brackets);
    2.51 -         in if is_none infrd_t' then
    2.52 +         in show_brackets := old_show_brackets;
    2.53 +            if is_none infrd_t' then
    2.54                process_terms ts (idx, infrd_t, tye) msg'' (n+1)
    2.55              else
    2.56                process_terms ts (Some n, infrd_t', tye') msg'' (n+1)
     3.1 --- a/src/Pure/tactic.ML	Sat Mar 11 17:46:14 1995 +0100
     3.2 +++ b/src/Pure/tactic.ML	Mon Mar 13 09:38:10 1995 +0100
     3.3 @@ -197,9 +197,11 @@
     3.4      val rts = types_sorts rule and (types,sorts) = types_sorts state
     3.5      fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
     3.6        | types'(ixn) = types ixn;
     3.7 -    val (Tinsts,insts) = read_insts sign rts (types',sorts) sinsts
     3.8 +    val used = add_term_tvarnames
     3.9 +                  (#prop(rep_thm state) $ #prop(rep_thm rule),[])
    3.10 +    val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
    3.11  in instantiate (map lifttvar Tinsts, map liftpair insts)
    3.12 -		(lift_rule (state,i) rule)
    3.13 +               (lift_rule (state,i) rule)
    3.14  end;
    3.15  
    3.16  
     4.1 --- a/src/Pure/term.ML	Sat Mar 11 17:46:14 1995 +0100
     4.2 +++ b/src/Pure/term.ML	Mon Mar 13 09:38:10 1995 +0100
     4.3 @@ -189,7 +189,14 @@
     4.4    | size_of_term (f$t) = size_of_term f  +  size_of_term t
     4.5    | size_of_term _ = 1;
     4.6  
     4.7 - 
     4.8 +fun map_type_tvar f (Type(a,Ts)) = Type(a, map (map_type_tvar f) Ts)
     4.9 +  | map_type_tvar f (T as TFree _) = T
    4.10 +  | map_type_tvar f (TVar x) = f x;
    4.11 +
    4.12 +fun map_type_tfree f (Type(a,Ts)) = Type(a, map (map_type_tfree f) Ts)
    4.13 +  | map_type_tfree f (TFree x) = f x
    4.14 +  | map_type_tfree f (T as TVar _) = T;
    4.15 +
    4.16  (* apply a function to all types in a term *)
    4.17  fun map_term_types f =
    4.18  let fun map(Const(a,T)) = Const(a, f T)
    4.19 @@ -432,9 +439,7 @@
    4.20  
    4.21  
    4.22  (* Increment the index of all Poly's in T by k *)
    4.23 -fun incr_tvar k (Type(a,Ts)) = Type(a, map (incr_tvar k) Ts)
    4.24 -  | incr_tvar k (T as TFree _) = T
    4.25 -  | incr_tvar k (TVar((a,i),rs)) = TVar((a,i+k),rs);
    4.26 +fun incr_tvar k = map_type_tvar (fn ((a,i),S) => TVar((a,i+k),S));
    4.27  
    4.28  
    4.29  (**** Syntax-related declarations ****)
    4.30 @@ -500,20 +505,40 @@
    4.31    | add_typ_tfrees(TFree(f),fs) = f ins fs
    4.32    | add_typ_tfrees(TVar(_),fs) = fs;
    4.33  
    4.34 +fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames (Ts,nms)
    4.35 +  | add_typ_varnames(TFree(nm,_),nms) = nm ins nms
    4.36 +  | add_typ_varnames(TVar((nm,_),_),nms) = nm ins nms;
    4.37 +
    4.38  (*Accumulates the TVars in a term, suppressing duplicates. *)
    4.39  val add_term_tvars = it_term_types add_typ_tvars;
    4.40 -val add_term_tvar_ixns = (map #1) o (it_term_types add_typ_tvars);
    4.41  
    4.42  (*Accumulates the TFrees in a term, suppressing duplicates. *)
    4.43  val add_term_tfrees = it_term_types add_typ_tfrees;
    4.44  val add_term_tfree_names = it_term_types add_typ_tfree_names;
    4.45  
    4.46 +val add_term_tvarnames = it_term_types add_typ_varnames;
    4.47 +
    4.48  (*Non-list versions*)
    4.49  fun typ_tfrees T = add_typ_tfrees(T,[]);
    4.50  fun typ_tvars T = add_typ_tvars(T,[]);
    4.51  fun term_tfrees t = add_term_tfrees(t,[]);
    4.52  fun term_tvars t = add_term_tvars(t,[]);
    4.53  
    4.54 +(*special code to enforce left-to-right collection of TVar-indexnames*)
    4.55 +
    4.56 +fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts)
    4.57 +  | add_typ_ixns(ixns,TVar(ixn,_)) = if ixn mem ixns then ixns else ixns@[ixn]
    4.58 +  | add_typ_ixns(ixns,TFree(_)) = ixns;
    4.59 +
    4.60 +fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
    4.61 +  | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
    4.62 +  | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
    4.63 +  | add_term_tvar_ixns(Bound _,ixns) = ixns
    4.64 +  | add_term_tvar_ixns(Abs(_,T,t),ixns) =
    4.65 +      add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
    4.66 +  | add_term_tvar_ixns(f$t,ixns) =
    4.67 +      add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
    4.68 +
    4.69  (** Frees and Vars **)
    4.70  
    4.71  (*a partial ordering (not reflexive) for atomic terms*)
     5.1 --- a/src/Pure/thm.ML	Sat Mar 11 17:46:14 1995 +0100
     5.2 +++ b/src/Pure/thm.ML	Mon Mar 13 09:38:10 1995 +0100
     5.3 @@ -106,7 +106,7 @@
     5.4    val cpure_thy		: theory
     5.5    val read_def_cterm 	:
     5.6           Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
     5.7 -         string * typ -> cterm * (indexname * typ) list
     5.8 +         string list -> bool -> string * typ -> cterm * (indexname * typ) list
     5.9     val reflexive	: cterm -> thm
    5.10    val rename_params_rule: string list * int -> thm -> thm
    5.11    val rep_thm		: thm -> {prop: term, hyps: term list, 
    5.12 @@ -193,17 +193,18 @@
    5.13  (** read cterms **)   (*exception ERROR*)
    5.14  
    5.15  (*read term, infer types, certify term*)
    5.16 -fun read_def_cterm (sign, types, sorts) (a, T) =
    5.17 +fun read_def_cterm (sign, types, sorts) used freeze (a, T) =
    5.18    let
    5.19      val T' = Sign.certify_typ sign T
    5.20        handle TYPE (msg, _, _) => error msg;
    5.21      val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
    5.22 -    val (_, t', tye) = Sign.infer_types sign types sorts true (ts, T');
    5.23 +    val (_, t', tye) =
    5.24 +          Sign.infer_types sign types sorts used freeze true (ts, T');
    5.25      val ct = cterm_of sign t'
    5.26        handle TERM (msg, _) => error msg;
    5.27    in (ct, tye) end;
    5.28  
    5.29 -fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None);
    5.30 +fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
    5.31  
    5.32  
    5.33  
    5.34 @@ -371,8 +372,10 @@
    5.35      handle ERROR => err_in_axm name;
    5.36  
    5.37  fun inferT_axm sg (name, pre_tm) =
    5.38 - (name, no_vars (#2 (Sign.infer_types sg (K None) (K None) true ([pre_tm], propT))))
    5.39 -    handle ERROR => err_in_axm name;
    5.40 +  let val t = #2(Sign.infer_types sg (K None) (K None) [] true true
    5.41 +                                     ([pre_tm], propT))
    5.42 +  in  (name, no_vars t) end
    5.43 +  handle ERROR => err_in_axm name;
    5.44  
    5.45  
    5.46  (* extend axioms of a theory *)
    5.47 @@ -758,7 +761,7 @@
    5.48  
    5.49  (* Replace all TVars by new TFrees *)
    5.50  fun freezeT(Thm{sign,maxidx,hyps,prop}) =
    5.51 -  let val prop' = Type.freeze (K true) prop
    5.52 +  let val prop' = Type.freeze prop
    5.53    in Thm{sign=sign, maxidx=maxidx_of_term prop', hyps=hyps, prop=prop'} end;
    5.54  
    5.55  
     6.1 --- a/src/Pure/type.ML	Sat Mar 11 17:46:14 1995 +0100
     6.2 +++ b/src/Pure/type.ML	Mon Mar 13 09:38:10 1995 +0100
     6.3 @@ -41,10 +41,12 @@
     6.4    val rem_sorts: typ -> typ
     6.5    val cert_typ: type_sig -> typ -> typ
     6.6    val norm_typ: type_sig -> typ -> typ
     6.7 -  val freeze: (indexname -> bool) -> term -> term
     6.8 +  val freeze: term -> term
     6.9    val freeze_vars: typ -> typ
    6.10 -  val infer_types: type_sig * (string -> typ option) * (indexname -> typ option) *
    6.11 -    (indexname -> sort option) * typ * term -> term * (indexname * typ) list
    6.12 +  val infer_types: type_sig * (string -> typ option) *
    6.13 +                   (indexname -> typ option) * (indexname -> sort option) *
    6.14 +                   string list * bool * typ * term
    6.15 +                   -> term * (indexname * typ) list
    6.16    val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
    6.17    val thaw_vars: typ -> typ
    6.18    val typ_errors: type_sig -> typ * string list -> string list
    6.19 @@ -72,9 +74,7 @@
    6.20    else raise_type "Illegal schematic type variable(s)" [T] [];
    6.21  
    6.22  (*turn TFrees into TVars to allow types & axioms to be written without "?"*)
    6.23 -fun varifyT (Type (a, Ts)) = Type (a, map varifyT Ts)
    6.24 -  | varifyT (TFree (a, S)) = TVar ((a, 0), S)
    6.25 -  | varifyT T = T;
    6.26 +val varifyT = map_type_tfree (fn (a, S) => TVar((a, 0), S));
    6.27  
    6.28  (*inverse of varifyT*)
    6.29  fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
    6.30 @@ -87,13 +87,10 @@
    6.31      val fs = add_term_tfree_names (t, []) \\ fixed;
    6.32      val ixns = add_term_tvar_ixns (t, []);
    6.33      val fmap = fs ~~ variantlist (fs, map #1 ixns)
    6.34 -    fun thaw (Type(a, Ts)) = Type (a, map thaw Ts)
    6.35 -      | thaw (T as TVar _) = T
    6.36 -      | thaw (T as TFree(a, S)) =
    6.37 -          (case assoc (fmap, a) of None => T | Some b => TVar((b, 0), S))
    6.38 -  in
    6.39 -    map_term_types thaw t
    6.40 -  end;
    6.41 +    fun thaw(f as (a,S)) = case assoc (fmap, a) of
    6.42 +                             None => TFree(f)
    6.43 +                           | Some b => TVar((b, 0), S)
    6.44 +  in  map_term_types (map_type_tfree thaw) t  end;
    6.45  
    6.46  
    6.47  
    6.48 @@ -298,11 +295,10 @@
    6.49  (*Instantiation of type variables in types*)
    6.50  (*Pre: instantiations obey restrictions! *)
    6.51  fun inst_typ tye =
    6.52 -  let fun inst(Type(a, Ts)) = Type(a, map inst Ts)
    6.53 -        | inst(T as TFree _) = T
    6.54 -        | inst(T as TVar(v, _)) =
    6.55 -            (case assoc(tye, v) of Some U => inst U | None => T)
    6.56 -  in inst end;
    6.57 +  let fun inst(var as (v, _)) = case assoc(tye, v) of
    6.58 +                                  Some U => inst_typ tye U
    6.59 +                                | None => TVar(var)
    6.60 +  in map_type_tvar inst end;
    6.61  
    6.62  (* 'least_sort' returns for a given type its maximum sort:
    6.63     - type variables, free types: the sort brought with
    6.64 @@ -327,11 +323,10 @@
    6.65  
    6.66  (*Instantiation of type variables in types *)
    6.67  fun inst_typ_tvars(tsig, tye) =
    6.68 -  let fun inst(Type(a, Ts)) = Type(a, map inst Ts)
    6.69 -        | inst(T as TFree _) = T
    6.70 -        | inst(T as TVar(v, S)) = (case assoc(tye, v) of
    6.71 -                None => T | Some(U) => (check_has_sort(tsig, U, S); U))
    6.72 -  in inst end;
    6.73 +  let fun inst(var as (v, S)) = case assoc(tye, v) of
    6.74 +              Some U => (check_has_sort(tsig, U, S); U)
    6.75 +            | None => TVar(var)
    6.76 +  in map_type_tvar inst end;
    6.77  
    6.78  (*Instantiation of type variables in terms *)
    6.79  fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye));
    6.80 @@ -927,9 +922,8 @@
    6.81             end
    6.82    in inf end;
    6.83  
    6.84 -fun freeze_vars(Type(a, Ts)) = Type(a, map freeze_vars Ts)
    6.85 -  | freeze_vars(T as TFree _) = T
    6.86 -  | freeze_vars(TVar(v, S)) = TFree(Syntax.string_of_vname v, S);
    6.87 +val freeze_vars =
    6.88 +      map_type_tvar (fn (v, S) => TFree(Syntax.string_of_vname v, S));
    6.89  
    6.90  (* Attach a type to a constant *)
    6.91  fun type_const (a, T) = Const(a, incr_tvar (new_tvar_inx()) T);
    6.92 @@ -1013,25 +1007,42 @@
    6.93    | unconstrain (f$t) = unconstrain f $ unconstrain t
    6.94    | unconstrain (t) = t;
    6.95  
    6.96 +fun nextname(pref,c) = if c="z" then (pref^"a", "a") else (pref,chr(ord(c)+1));
    6.97  
    6.98 -(* Turn all TVars which satisfy p into new TFrees *)
    6.99 -fun freeze p t =
   6.100 -  let val fs = add_term_tfree_names(t, []);
   6.101 -      val inxs = filter p (add_term_tvar_ixns(t, []));
   6.102 -      val vmap = inxs ~~ variantlist(map #1 inxs, fs);
   6.103 -      fun free(Type(a, Ts)) = Type(a, map free Ts)
   6.104 -        | free(T as TVar(v, S)) =
   6.105 -            (case assoc(vmap, v) of None => T | Some(a) => TFree(a, S))
   6.106 -        | free(T as TFree _) = T
   6.107 -  in map_term_types free t end;
   6.108 +fun newtvars used =
   6.109 +  let fun new([],_,vmap) = vmap
   6.110 +        | new(ixn::ixns,p as (pref,c),vmap) =
   6.111 +            let val nm = pref ^ c
   6.112 +            in if nm mem used then new(ixn::ixns,nextname p, vmap)
   6.113 +               else new(ixns, nextname p, (ixn,nm)::vmap)
   6.114 +            end
   6.115 +  in new end;
   6.116 +
   6.117 +(*
   6.118 +Turn all TVars which satisfy p into new (if freeze then TFrees else TVars).
   6.119 +Note that if t contains frozen TVars there is the possibility that a TVar is
   6.120 +turned into one of those. This is sound but not complete.
   6.121 +*)
   6.122 +fun convert used freeze p t =
   6.123 +  let val used = if freeze then add_term_tfree_names(t, used)
   6.124 +                 else used union
   6.125 +                      (map #1 (filter_out p (add_term_tvar_ixns(t, []))))
   6.126 +      val ixns = filter p (add_term_tvar_ixns(t, []));
   6.127 +      val vmap = newtvars used (ixns,("'","a"),[]);
   6.128 +      fun conv(var as (ixn,S)) = case assoc(vmap,ixn) of
   6.129 +            None => TVar(var) |
   6.130 +            Some(a) => if freeze then TFree(a,S) else TVar((a,0),S);
   6.131 +  in map_term_types (map_type_tvar conv) t end;
   6.132 +
   6.133 +fun freeze t = convert (add_term_tfree_names(t,[])) true (K true) t;
   6.134  
   6.135  (* Thaw all TVars that were frozen in freeze_vars *)
   6.136 -fun thaw_vars(Type(a, Ts)) = Type(a, map thaw_vars Ts)
   6.137 -  | thaw_vars(T as TFree(a, S)) = (case explode a of
   6.138 +val thaw_vars =
   6.139 +  let fun thaw(f as (a, S)) = (case explode a of
   6.140            "?"::"'"::vn => let val ((b, i), _) = Syntax.scan_varname vn
   6.141                            in TVar(("'"^b, i), S) end
   6.142 -        | _ => T)
   6.143 -  | thaw_vars(T) = T;
   6.144 +        | _ => TFree f)
   6.145 +  in map_type_tfree thaw end;
   6.146  
   6.147  
   6.148  fun restrict tye =
   6.149 @@ -1041,8 +1052,8 @@
   6.150  
   6.151  
   6.152  (*Infer types for term t using tables. Check that t's type and T unify *)
   6.153 -
   6.154 -fun infer_term (tsig, const_type, types, sorts, T, t) =
   6.155 +(*freeze determines if internal TVars are turned into TFrees or TVars*)
   6.156 +fun infer_term (tsig, const_type, types, sorts, used, freeze, T, t) =
   6.157    let
   6.158      val u = attach_types (tsig, const_type, types, sorts) t;
   6.159      val (U, tye) = infer tsig ([], u, []);
   6.160 @@ -1053,8 +1064,8 @@
   6.161      val all = Const("", Type("", map snd Ttye)) $ (inst_types tye' uu)
   6.162        (*all is a dummy term which contains all exported TVars*)
   6.163      val Const(_, Type(_, Ts)) $ u'' =
   6.164 -      map_term_types thaw_vars (freeze (fn (_, i) => i < 0) all)
   6.165 -      (*turn all internally generated TVars into TFrees
   6.166 +      map_term_types thaw_vars (convert used freeze (fn (_, i) => i < 0) all)
   6.167 +      (*convert all internally generated TVars into TFrees or TVars
   6.168          and thaw all initially frozen TVars*)
   6.169    in
   6.170      (u'', (map fst Ttye) ~~ Ts)
   6.171 @@ -1064,4 +1075,3 @@
   6.172  
   6.173  
   6.174  end;
   6.175 -