renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
authorwenzelm
Fri Sep 15 22:56:13 2006 +0200 (2006-09-15)
changeset 205488ef25fe585a8
parent 20547 796ae7fa1049
child 20549 c643984eb94b
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
TFL/tfl.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/specification_package.ML
src/Provers/IsaPlanner/isand.ML
src/Provers/IsaPlanner/rw_tools.ML
src/Pure/Isar/element.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Tools/class_package.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/compress.ML
src/Pure/consts.ML
src/Pure/envir.ML
src/Pure/logic.ML
src/Pure/proofterm.ML
src/Pure/sign.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/unify.ML
     1.1 --- a/TFL/tfl.ML	Fri Sep 15 22:56:08 2006 +0200
     1.2 +++ b/TFL/tfl.ML	Fri Sep 15 22:56:13 2006 +0200
     1.3 @@ -389,8 +389,8 @@
     1.4                                               quote fid ^ " but found one of " ^
     1.5                                        quote x)
     1.6                      else x ^ "_def"
     1.7 -     val wfrec_R_M =  map_term_types poly_tvars
     1.8 -                          (wfrec $ map_term_types poly_tvars R)
     1.9 +     val wfrec_R_M =  map_types poly_tvars
    1.10 +                          (wfrec $ map_types poly_tvars R)
    1.11                        $ functional
    1.12       val def_term = mk_const_def (Theory.sign_of thy) (x, Ty, wfrec_R_M)
    1.13       val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Sep 15 22:56:08 2006 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Sep 15 22:56:13 2006 +0200
     2.3 @@ -530,7 +530,7 @@
     2.4          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
     2.5             (fn (S, x) =>
     2.6                let
     2.7 -                val S = map_term_types (map_type_tfree
     2.8 +                val S = map_types (map_type_tfree
     2.9                    (fn (s, cs) => TFree (s, cs union cp_classes))) S;
    2.10                  val T = HOLogic.dest_setT (fastype_of S);
    2.11                  val permT = mk_permT (Type (name, []))
     3.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Sep 15 22:56:08 2006 +0200
     3.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Sep 15 22:56:13 2006 +0200
     3.3 @@ -170,7 +170,7 @@
     3.4    (let
     3.5      val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
     3.6      fun varify (t, (i, ts)) =
     3.7 -      let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
     3.8 +      let val t' = map_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
     3.9        in (maxidx_of_term t', t'::ts) end;
    3.10      val (i, cs') = foldr varify (~1, []) cs;
    3.11      val (i', intr_ts') = foldr varify (i, []) intr_ts;
    3.12 @@ -180,7 +180,7 @@
    3.13        let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
    3.14        in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
    3.15      val (env, _) = fold unify rec_consts (Vartab.empty, i');
    3.16 -    val subst = Type.freeze o map_term_types (Envir.norm_type env)
    3.17 +    val subst = Type.freeze o map_types (Envir.norm_type env)
    3.18  
    3.19    in (map subst cs', map subst intr_ts')
    3.20    end) handle Type.TUNIFY =>
     4.1 --- a/src/HOL/Tools/refute.ML	Fri Sep 15 22:56:08 2006 +0200
     4.2 +++ b/src/HOL/Tools/refute.ML	Fri Sep 15 22:56:13 2006 +0200
     4.3 @@ -446,7 +446,7 @@
     4.4  				  SOME x => x
     4.5  				| NONE   => raise Type.TYPE_MATCH (* no match found - perhaps due to sort constraints *))
     4.6  		in
     4.7 -			map_term_types
     4.8 +			map_types
     4.9  				(map_type_tvar
    4.10  					(fn v =>
    4.11  						case Type.lookup (typeSubs, v) of
    4.12 @@ -461,7 +461,7 @@
    4.13  		(* term 't'                                                            *)
    4.14  		(* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *)
    4.15  		fun monomorphic_term typeSubs t =
    4.16 -			map_term_types (map_type_tvar
    4.17 +			map_types (map_type_tvar
    4.18  				(fn v =>
    4.19  					case Type.lookup (typeSubs, v) of
    4.20  					  NONE =>
     5.1 --- a/src/HOL/Tools/specification_package.ML	Fri Sep 15 22:56:08 2006 +0200
     5.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Sep 15 22:56:13 2006 +0200
     5.3 @@ -108,7 +108,7 @@
     5.4                   NONE => TVar f
     5.5                 | SOME (b, _) => TFree (b, S))
     5.6      in
     5.7 -        map_term_types (map_type_tvar unthaw) t
     5.8 +        map_types (map_type_tvar unthaw) t
     5.9      end
    5.10  
    5.11  (* The syntactic meddling needed to setup add_specification for work *)
     6.1 --- a/src/Provers/IsaPlanner/isand.ML	Fri Sep 15 22:56:08 2006 +0200
     6.2 +++ b/src/Provers/IsaPlanner/isand.ML	Fri Sep 15 22:56:13 2006 +0200
     6.3 @@ -173,7 +173,7 @@
     6.4      in trec ty end;
     6.5  
     6.6  (* implicit types and term *)
     6.7 -fun allify_term_typs ty = Term.map_term_types (allify_typ ty);
     6.8 +fun allify_term_typs ty = Term.map_types (allify_typ ty);
     6.9  
    6.10  (* allified version of term, given frees to allify over. Note that we
    6.11  only allify over the types on the given allified cterm, we can't do
     7.1 --- a/src/Provers/IsaPlanner/rw_tools.ML	Fri Sep 15 22:56:08 2006 +0200
     7.2 +++ b/src/Provers/IsaPlanner/rw_tools.ML	Fri Sep 15 22:56:13 2006 +0200
     7.3 @@ -120,7 +120,7 @@
     7.4  (* map a function f to each type variable in a term *)
     7.5  (* implicit arg: term *)
     7.6  fun map_to_term_tvars f =
     7.7 -    Term.map_term_types (fn TVar(ix,ty) => f (ix,ty) | x => x);
     7.8 +    Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x);   (* FIXME map_atyps !? *)
     7.9  
    7.10  
    7.11  
     8.1 --- a/src/Pure/Isar/element.ML	Fri Sep 15 22:56:08 2006 +0200
     8.2 +++ b/src/Pure/Isar/element.ML	Fri Sep 15 22:56:13 2006 +0200
     8.3 @@ -381,7 +381,7 @@
     8.4  
     8.5  fun instT_term env =
     8.6    if Symtab.is_empty env then I
     8.7 -  else Term.map_term_types (instT_type env);
     8.8 +  else Term.map_types (instT_type env);
     8.9  
    8.10  fun instT_subst env th = (Drule.fold_terms o Term.fold_types o Term.fold_atyps)
    8.11    (fn T as TFree (a, _) =>
     9.1 --- a/src/Pure/Isar/locale.ML	Fri Sep 15 22:56:08 2006 +0200
     9.2 +++ b/src/Pure/Isar/locale.ML	Fri Sep 15 22:56:13 2006 +0200
     9.3 @@ -2119,7 +2119,7 @@
     9.4              TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s));
     9.5      val rename =
     9.6            if is_local then I
     9.7 -          else Term.map_term_types renameT;
     9.8 +          else Term.map_types renameT;
     9.9  
    9.10      val tinst = Symtab.make (map
    9.11                  (fn ((x, 0), T) => (x, T |> renameT)
    10.1 --- a/src/Pure/Isar/rule_insts.ML	Fri Sep 15 22:56:08 2006 +0200
    10.2 +++ b/src/Pure/Isar/rule_insts.ML	Fri Sep 15 22:56:13 2006 +0200
    10.3 @@ -97,7 +97,7 @@
    10.4      val instT2 = Envir.norm_type
    10.5        (#1 (fold (unify_vartypes thy vars1) internal_insts (Vartab.empty, 0)));
    10.6      val vars2 = map (apsnd instT2) vars1;
    10.7 -    val internal_insts2 = map (apsnd (map_term_types instT2)) internal_insts;
    10.8 +    val internal_insts2 = map (apsnd (map_types instT2)) internal_insts;
    10.9      val inst2 = instantiate internal_insts2;
   10.10  
   10.11  
   10.12 @@ -110,7 +110,7 @@
   10.13  
   10.14      val instT3 = Term.typ_subst_TVars inferred;
   10.15      val vars3 = map (apsnd instT3) vars2;
   10.16 -    val internal_insts3 = map (apsnd (map_term_types instT3)) internal_insts2;
   10.17 +    val internal_insts3 = map (apsnd (map_types instT3)) internal_insts2;
   10.18      val external_insts3 = xs ~~ ts;
   10.19      val inst3 = instantiate external_insts3;
   10.20  
    11.1 --- a/src/Pure/Proof/extraction.ML	Fri Sep 15 22:56:08 2006 +0200
    11.2 +++ b/src/Pure/Proof/extraction.ML	Fri Sep 15 22:56:13 2006 +0200
    11.3 @@ -277,7 +277,7 @@
    11.4    | freeze T = T;
    11.5  
    11.6  fun freeze_thaw f x =
    11.7 -  map_term_types thaw (f (map_term_types freeze x));
    11.8 +  map_types thaw (f (map_types freeze x));
    11.9  
   11.10  fun etype_of thy vs Ts t =
   11.11    let
   11.12 @@ -324,7 +324,7 @@
   11.13        val T = etype_of thy' vs [] prop;
   11.14        val (T', thw) = Type.freeze_thaw_type
   11.15          (if T = nullT then nullT else map fastype_of vars' ---> T);
   11.16 -      val t = map_term_types thw (term_of (read_cterm thy' (s1, T')));
   11.17 +      val t = map_types thw (term_of (read_cterm thy' (s1, T')));
   11.18        val r' = freeze_thaw (condrew thy' eqns
   11.19          (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
   11.20            (Const ("realizes", T --> propT --> propT) $
    12.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Sep 15 22:56:08 2006 +0200
    12.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Sep 15 22:56:13 2006 +0200
    12.3 @@ -128,7 +128,7 @@
    12.4      val thms = PureThy.all_thms_of thy;
    12.5      val axms = Theory.all_axioms_of thy;
    12.6  
    12.7 -    fun mk_term t = (if ty then I else map_term_types (K dummyT))
    12.8 +    fun mk_term t = (if ty then I else map_types (K dummyT))
    12.9        (Term.no_dummy_patterns t);
   12.10  
   12.11      fun prf_of [] (Bound i) = PBound i
    13.1 --- a/src/Pure/Proof/reconstruct.ML	Fri Sep 15 22:56:08 2006 +0200
    13.2 +++ b/src/Pure/Proof/reconstruct.ML	Fri Sep 15 22:56:13 2006 +0200
    13.3 @@ -379,7 +379,7 @@
    13.4                if p mem tfrees then TVar ((a, ~1), S) else TFree p)
    13.5            in
    13.6              (maxidx', prfs', map_proof_terms (subst_TVars tye o
    13.7 -               map_term_types varify) (typ_subst_TVars tye o varify) prf)
    13.8 +               map_types varify) (typ_subst_TVars tye o varify) prf)
    13.9            end
   13.10        | expand maxidx prfs prf = (maxidx, prfs, prf);
   13.11  
    14.1 --- a/src/Pure/Tools/class_package.ML	Fri Sep 15 22:56:08 2006 +0200
    14.2 +++ b/src/Pure/Tools/class_package.ML	Fri Sep 15 22:56:13 2006 +0200
    14.3 @@ -416,7 +416,7 @@
    14.4              val t' = case mk_typnorm thy_read (ty', ty)
    14.5               of NONE => error ("superfluous definition for constant " ^
    14.6                    quote c ^ "::" ^ Sign.string_of_typ thy_read ty)
    14.7 -              | SOME norm => map_term_types norm t
    14.8 +              | SOME norm => map_types norm t
    14.9            in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
   14.10        in fold_map read defs cs end;
   14.11      val (defs, _) = assume_arities_thy theory arities_pair (read_defs raw_defs cs);
    15.1 --- a/src/Pure/axclass.ML	Fri Sep 15 22:56:08 2006 +0200
    15.2 +++ b/src/Pure/axclass.ML	Fri Sep 15 22:56:13 2006 +0200
    15.3 @@ -285,7 +285,7 @@
    15.4              " needs to be weaker than " ^ Pretty.string_of_sort pp super)
    15.5        | [] => t
    15.6        | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t))
    15.7 -      |> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
    15.8 +      |> map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
    15.9        |> Logic.close_form;
   15.10  
   15.11      val axiomss = prep_propp (ctxt, map (map (rpair []) o snd) raw_specs)
    16.1 --- a/src/Pure/codegen.ML	Fri Sep 15 22:56:08 2006 +0200
    16.2 +++ b/src/Pure/codegen.ML	Fri Sep 15 22:56:13 2006 +0200
    16.3 @@ -1010,7 +1010,7 @@
    16.4        | strip t = t;
    16.5      val (gi, frees) = Logic.goal_params
    16.6        (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
    16.7 -    val gi' = ObjectLogic.atomize_term thy (map_term_types
    16.8 +    val gi' = ObjectLogic.atomize_term thy (map_types
    16.9        (map_type_tfree (fn p as (s, _) =>
   16.10          the_default (the_default (TFree p) default_type)
   16.11            (AList.lookup (op =) tvinsts s))) (subst_bounds (frees, strip gi)));
    17.1 --- a/src/Pure/compress.ML	Fri Sep 15 22:56:08 2006 +0200
    17.2 +++ b/src/Pure/compress.ML	Fri Sep 15 22:56:13 2006 +0200
    17.3 @@ -61,6 +61,6 @@
    17.4            (case Termtab.lookup (! terms) t of
    17.5              SOME t' => t'
    17.6            | NONE => (change terms (Termtab.update (t, t)); t));
    17.7 -  in compress o map_term_types (typ thy) end;
    17.8 +  in compress o map_types (typ thy) end;
    17.9  
   17.10  end;
    18.1 --- a/src/Pure/consts.ML	Fri Sep 15 22:56:08 2006 +0200
    18.2 +++ b/src/Pure/consts.ML	Fri Sep 15 22:56:13 2006 +0200
    18.3 @@ -250,7 +250,7 @@
    18.4  fun abbreviate pp tsig naming mode ((c, raw_rhs), authentic) consts =
    18.5    let
    18.6      val rhs = raw_rhs
    18.7 -      |> Term.map_term_types (Type.cert_typ tsig)
    18.8 +      |> Term.map_types (Type.cert_typ tsig)
    18.9        |> certify pp tsig (consts |> expand_abbrevs false);
   18.10      val rhs' = rhs
   18.11        |> certify pp tsig (consts |> expand_abbrevs true);
    19.1 --- a/src/Pure/envir.ML	Fri Sep 15 22:56:08 2006 +0200
    19.2 +++ b/src/Pure/envir.ML	Fri Sep 15 22:56:13 2006 +0200
    19.3 @@ -268,7 +268,7 @@
    19.4    in subst T end;
    19.5  
    19.6  (*Substitute for type Vars in a term*)
    19.7 -val subst_TVars = map_term_types o typ_subst_TVars;
    19.8 +val subst_TVars = map_types o typ_subst_TVars;
    19.9  
   19.10  (*Substitute for Vars in a term *)
   19.11  fun subst_Vars itms t = if Vartab.is_empty itms then t else
    20.1 --- a/src/Pure/logic.ML	Fri Sep 15 22:56:08 2006 +0200
    20.2 +++ b/src/Pure/logic.ML	Fri Sep 15 22:56:13 2006 +0200
    20.3 @@ -555,7 +555,7 @@
    20.4      (fn Free (x, T) => Var ((x, 0), T)
    20.5        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    20.6        | t => t)
    20.7 -  |> Term.map_term_types varifyT
    20.8 +  |> Term.map_types varifyT
    20.9    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   20.10  
   20.11  fun unvarify tm =
   20.12 @@ -564,7 +564,7 @@
   20.13        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   20.14        | Free (x, _) => raise TERM (bad_fixed x, [tm])
   20.15        | t => t)
   20.16 -  |> Term.map_term_types unvarifyT
   20.17 +  |> Term.map_types unvarifyT
   20.18    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   20.19  
   20.20  val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
   20.21 @@ -572,11 +572,11 @@
   20.22  
   20.23  val legacy_varify =
   20.24    Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
   20.25 -  Term.map_term_types legacy_varifyT;
   20.26 +  Term.map_types legacy_varifyT;
   20.27  
   20.28  val legacy_unvarify =
   20.29    Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
   20.30 -  Term.map_term_types legacy_unvarifyT;
   20.31 +  Term.map_types legacy_unvarifyT;
   20.32  
   20.33  
   20.34  (* goal states *)
    21.1 --- a/src/Pure/proofterm.ML	Fri Sep 15 22:56:08 2006 +0200
    21.2 +++ b/src/Pure/proofterm.ML	Fri Sep 15 22:56:13 2006 +0200
    21.3 @@ -604,7 +604,7 @@
    21.4        (case AList.lookup (op =) fmap f of
    21.5          NONE => TFree f
    21.6        | SOME b => TVar ((b, 0), S));
    21.7 -  in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
    21.8 +  in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
    21.9    end;
   21.10  
   21.11  
   21.12 @@ -630,7 +630,7 @@
   21.13        [] => prf (*nothing to do!*)
   21.14      | _ =>
   21.15        let val frzT = map_type_tvar (freeze_one alist)
   21.16 -      in map_proof_terms (map_term_types frzT) frzT prf end)
   21.17 +      in map_proof_terms (map_types frzT) frzT prf end)
   21.18    end;
   21.19  
   21.20  end;
    22.1 --- a/src/Pure/sign.ML	Fri Sep 15 22:56:08 2006 +0200
    22.2 +++ b/src/Pure/sign.ML	Fri Sep 15 22:56:13 2006 +0200
    22.3 @@ -461,7 +461,7 @@
    22.4    let
    22.5      val _ = Context.check_thy thy;
    22.6      val _ = check_vars tm;
    22.7 -    val tm' = Term.map_term_types (certify_typ thy) tm;
    22.8 +    val tm' = Term.map_types (certify_typ thy) tm;
    22.9      val T = type_check pp tm';
   22.10      val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
   22.11      val tm'' = Consts.certify pp (tsig_of thy) consts tm';
    23.1 --- a/src/Pure/term.ML	Fri Sep 15 22:56:08 2006 +0200
    23.2 +++ b/src/Pure/term.ML	Fri Sep 15 22:56:13 2006 +0200
    23.3 @@ -68,7 +68,7 @@
    23.4    val map_aterms: (term -> term) -> term -> term
    23.5    val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    23.6    val map_type_tfree: (string * sort -> typ) -> typ -> typ
    23.7 -  val map_term_types: (typ -> typ) -> term -> term
    23.8 +  val map_types: (typ -> typ) -> term -> term
    23.9    val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
   23.10    val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
   23.11    val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
   23.12 @@ -423,7 +423,7 @@
   23.13  fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
   23.14  fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
   23.15  
   23.16 -fun map_term_types f =
   23.17 +fun map_types f =
   23.18    let
   23.19      fun map_aux (Const (a, T)) = Const (a, f T)
   23.20        | map_aux (Free (a, T)) = Free (a, f T)
   23.21 @@ -911,7 +911,7 @@
   23.22        in subst ty end;
   23.23  
   23.24  fun subst_atomic_types [] tm = tm
   23.25 -  | subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm;
   23.26 +  | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
   23.27  
   23.28  fun typ_subst_TVars [] ty = ty
   23.29    | typ_subst_TVars inst ty =
   23.30 @@ -922,7 +922,7 @@
   23.31        in subst ty end;
   23.32  
   23.33  fun subst_TVars [] tm = tm
   23.34 -  | subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm;
   23.35 +  | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
   23.36  
   23.37  fun subst_Vars [] tm = tm
   23.38    | subst_Vars inst tm =
    24.1 --- a/src/Pure/thm.ML	Fri Sep 15 22:56:08 2006 +0200
    24.2 +++ b/src/Pure/thm.ML	Fri Sep 15 22:56:13 2006 +0200
    24.3 @@ -1138,7 +1138,7 @@
    24.4      val ((x, i), S) = Term.dest_TVar T handle TYPE _ =>
    24.5        raise THM ("unconstrainT: not a type variable", 0, [th]);
    24.6      val T' = TVar ((x, i), []);
    24.7 -    val unconstrain = Term.map_term_types (Term.map_atyps (fn U => if U = T then T' else U));
    24.8 +    val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
    24.9      val constraints = map (curry Logic.mk_inclass T') S;
   24.10    in
   24.11      Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
    25.1 --- a/src/Pure/type.ML	Fri Sep 15 22:56:08 2006 +0200
    25.2 +++ b/src/Pure/type.ML	Fri Sep 15 22:56:13 2006 +0200
    25.3 @@ -238,7 +238,7 @@
    25.4        (case AList.lookup (op =) fmap f of
    25.5          NONE => TFree f
    25.6        | SOME xi => TVar (xi, S));
    25.7 -  in (map_term_types (map_type_tfree thaw) t, fmap) end;
    25.8 +  in (map_types (map_type_tfree thaw) t, fmap) end;
    25.9  
   25.10  
   25.11  (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)
   25.12 @@ -277,8 +277,8 @@
   25.13    in
   25.14      (case alist of
   25.15        [] => (t, fn x => x) (*nothing to do!*)
   25.16 -    | _ => (map_term_types (map_type_tvar (freeze_one alist)) t,
   25.17 -      map_term_types (map_type_tfree (thaw_one (map swap alist)))))
   25.18 +    | _ => (map_types (map_type_tvar (freeze_one alist)) t,
   25.19 +      map_types (map_type_tfree (thaw_one (map swap alist)))))
   25.20    end;
   25.21  
   25.22  val freeze = #1 o freeze_thaw;
    26.1 --- a/src/Pure/unify.ML	Fri Sep 15 22:56:08 2006 +0200
    26.2 +++ b/src/Pure/unify.ML	Fri Sep 15 22:56:13 2006 +0200
    26.3 @@ -636,7 +636,7 @@
    26.4            Term.map_atyps (fn T as TVar ((x, i), S) =>
    26.5              if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
    26.6          val decr_indexes =
    26.7 -          Term.map_term_types decr_indexesT #>
    26.8 +          Term.map_types decr_indexesT #>
    26.9            Term.map_aterms (fn t as Var ((x, i), T) =>
   26.10              if i > maxidx then Var ((x, i - offset), T) else t | t => t);
   26.11