renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
--- a/TFL/tfl.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/TFL/tfl.ML Fri Sep 15 22:56:13 2006 +0200
@@ -389,8 +389,8 @@
quote fid ^ " but found one of " ^
quote x)
else x ^ "_def"
- val wfrec_R_M = map_term_types poly_tvars
- (wfrec $ map_term_types poly_tvars R)
+ val wfrec_R_M = map_types poly_tvars
+ (wfrec $ map_types poly_tvars R)
$ functional
val def_term = mk_const_def (Theory.sign_of thy) (x, Ty, wfrec_R_M)
val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
--- a/src/HOL/Nominal/nominal_package.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Fri Sep 15 22:56:13 2006 +0200
@@ -530,7 +530,7 @@
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
(fn (S, x) =>
let
- val S = map_term_types (map_type_tfree
+ val S = map_types (map_type_tfree
(fn (s, cs) => TFree (s, cs union cp_classes))) S;
val T = HOLogic.dest_setT (fastype_of S);
val permT = mk_permT (Type (name, []))
--- a/src/HOL/Tools/inductive_package.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/HOL/Tools/inductive_package.ML Fri Sep 15 22:56:13 2006 +0200
@@ -170,7 +170,7 @@
(let
val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
fun varify (t, (i, ts)) =
- let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
+ let val t' = map_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
in (maxidx_of_term t', t'::ts) end;
val (i, cs') = foldr varify (~1, []) cs;
val (i', intr_ts') = foldr varify (i, []) intr_ts;
@@ -180,7 +180,7 @@
let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
val (env, _) = fold unify rec_consts (Vartab.empty, i');
- val subst = Type.freeze o map_term_types (Envir.norm_type env)
+ val subst = Type.freeze o map_types (Envir.norm_type env)
in (map subst cs', map subst intr_ts')
end) handle Type.TUNIFY =>
--- a/src/HOL/Tools/refute.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/HOL/Tools/refute.ML Fri Sep 15 22:56:13 2006 +0200
@@ -446,7 +446,7 @@
SOME x => x
| NONE => raise Type.TYPE_MATCH (* no match found - perhaps due to sort constraints *))
in
- map_term_types
+ map_types
(map_type_tvar
(fn v =>
case Type.lookup (typeSubs, v) of
@@ -461,7 +461,7 @@
(* term 't' *)
(* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *)
fun monomorphic_term typeSubs t =
- map_term_types (map_type_tvar
+ map_types (map_type_tvar
(fn v =>
case Type.lookup (typeSubs, v) of
NONE =>
--- a/src/HOL/Tools/specification_package.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/HOL/Tools/specification_package.ML Fri Sep 15 22:56:13 2006 +0200
@@ -108,7 +108,7 @@
NONE => TVar f
| SOME (b, _) => TFree (b, S))
in
- map_term_types (map_type_tvar unthaw) t
+ map_types (map_type_tvar unthaw) t
end
(* The syntactic meddling needed to setup add_specification for work *)
--- a/src/Provers/IsaPlanner/isand.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Provers/IsaPlanner/isand.ML Fri Sep 15 22:56:13 2006 +0200
@@ -173,7 +173,7 @@
in trec ty end;
(* implicit types and term *)
-fun allify_term_typs ty = Term.map_term_types (allify_typ ty);
+fun allify_term_typs ty = Term.map_types (allify_typ ty);
(* allified version of term, given frees to allify over. Note that we
only allify over the types on the given allified cterm, we can't do
--- a/src/Provers/IsaPlanner/rw_tools.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Provers/IsaPlanner/rw_tools.ML Fri Sep 15 22:56:13 2006 +0200
@@ -120,7 +120,7 @@
(* map a function f to each type variable in a term *)
(* implicit arg: term *)
fun map_to_term_tvars f =
- Term.map_term_types (fn TVar(ix,ty) => f (ix,ty) | x => x);
+ Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x); (* FIXME map_atyps !? *)
--- a/src/Pure/Isar/element.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Isar/element.ML Fri Sep 15 22:56:13 2006 +0200
@@ -381,7 +381,7 @@
fun instT_term env =
if Symtab.is_empty env then I
- else Term.map_term_types (instT_type env);
+ else Term.map_types (instT_type env);
fun instT_subst env th = (Drule.fold_terms o Term.fold_types o Term.fold_atyps)
(fn T as TFree (a, _) =>
--- a/src/Pure/Isar/locale.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Isar/locale.ML Fri Sep 15 22:56:13 2006 +0200
@@ -2119,7 +2119,7 @@
TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s));
val rename =
if is_local then I
- else Term.map_term_types renameT;
+ else Term.map_types renameT;
val tinst = Symtab.make (map
(fn ((x, 0), T) => (x, T |> renameT)
--- a/src/Pure/Isar/rule_insts.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Isar/rule_insts.ML Fri Sep 15 22:56:13 2006 +0200
@@ -97,7 +97,7 @@
val instT2 = Envir.norm_type
(#1 (fold (unify_vartypes thy vars1) internal_insts (Vartab.empty, 0)));
val vars2 = map (apsnd instT2) vars1;
- val internal_insts2 = map (apsnd (map_term_types instT2)) internal_insts;
+ val internal_insts2 = map (apsnd (map_types instT2)) internal_insts;
val inst2 = instantiate internal_insts2;
@@ -110,7 +110,7 @@
val instT3 = Term.typ_subst_TVars inferred;
val vars3 = map (apsnd instT3) vars2;
- val internal_insts3 = map (apsnd (map_term_types instT3)) internal_insts2;
+ val internal_insts3 = map (apsnd (map_types instT3)) internal_insts2;
val external_insts3 = xs ~~ ts;
val inst3 = instantiate external_insts3;
--- a/src/Pure/Proof/extraction.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Sep 15 22:56:13 2006 +0200
@@ -277,7 +277,7 @@
| freeze T = T;
fun freeze_thaw f x =
- map_term_types thaw (f (map_term_types freeze x));
+ map_types thaw (f (map_types freeze x));
fun etype_of thy vs Ts t =
let
@@ -324,7 +324,7 @@
val T = etype_of thy' vs [] prop;
val (T', thw) = Type.freeze_thaw_type
(if T = nullT then nullT else map fastype_of vars' ---> T);
- val t = map_term_types thw (term_of (read_cterm thy' (s1, T')));
+ val t = map_types thw (term_of (read_cterm thy' (s1, T')));
val r' = freeze_thaw (condrew thy' eqns
(procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
(Const ("realizes", T --> propT --> propT) $
--- a/src/Pure/Proof/proof_syntax.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Fri Sep 15 22:56:13 2006 +0200
@@ -128,7 +128,7 @@
val thms = PureThy.all_thms_of thy;
val axms = Theory.all_axioms_of thy;
- fun mk_term t = (if ty then I else map_term_types (K dummyT))
+ fun mk_term t = (if ty then I else map_types (K dummyT))
(Term.no_dummy_patterns t);
fun prf_of [] (Bound i) = PBound i
--- a/src/Pure/Proof/reconstruct.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Proof/reconstruct.ML Fri Sep 15 22:56:13 2006 +0200
@@ -379,7 +379,7 @@
if p mem tfrees then TVar ((a, ~1), S) else TFree p)
in
(maxidx', prfs', map_proof_terms (subst_TVars tye o
- map_term_types varify) (typ_subst_TVars tye o varify) prf)
+ map_types varify) (typ_subst_TVars tye o varify) prf)
end
| expand maxidx prfs prf = (maxidx, prfs, prf);
--- a/src/Pure/Tools/class_package.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Tools/class_package.ML Fri Sep 15 22:56:13 2006 +0200
@@ -416,7 +416,7 @@
val t' = case mk_typnorm thy_read (ty', ty)
of NONE => error ("superfluous definition for constant " ^
quote c ^ "::" ^ Sign.string_of_typ thy_read ty)
- | SOME norm => map_term_types norm t
+ | SOME norm => map_types norm t
in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
in fold_map read defs cs end;
val (defs, _) = assume_arities_thy theory arities_pair (read_defs raw_defs cs);
--- a/src/Pure/axclass.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/axclass.ML Fri Sep 15 22:56:13 2006 +0200
@@ -285,7 +285,7 @@
" needs to be weaker than " ^ Pretty.string_of_sort pp super)
| [] => t
| _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t))
- |> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
+ |> map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
|> Logic.close_form;
val axiomss = prep_propp (ctxt, map (map (rpair []) o snd) raw_specs)
--- a/src/Pure/codegen.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/codegen.ML Fri Sep 15 22:56:13 2006 +0200
@@ -1010,7 +1010,7 @@
| strip t = t;
val (gi, frees) = Logic.goal_params
(prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
- val gi' = ObjectLogic.atomize_term thy (map_term_types
+ val gi' = ObjectLogic.atomize_term thy (map_types
(map_type_tfree (fn p as (s, _) =>
the_default (the_default (TFree p) default_type)
(AList.lookup (op =) tvinsts s))) (subst_bounds (frees, strip gi)));
--- a/src/Pure/compress.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/compress.ML Fri Sep 15 22:56:13 2006 +0200
@@ -61,6 +61,6 @@
(case Termtab.lookup (! terms) t of
SOME t' => t'
| NONE => (change terms (Termtab.update (t, t)); t));
- in compress o map_term_types (typ thy) end;
+ in compress o map_types (typ thy) end;
end;
--- a/src/Pure/consts.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/consts.ML Fri Sep 15 22:56:13 2006 +0200
@@ -250,7 +250,7 @@
fun abbreviate pp tsig naming mode ((c, raw_rhs), authentic) consts =
let
val rhs = raw_rhs
- |> Term.map_term_types (Type.cert_typ tsig)
+ |> Term.map_types (Type.cert_typ tsig)
|> certify pp tsig (consts |> expand_abbrevs false);
val rhs' = rhs
|> certify pp tsig (consts |> expand_abbrevs true);
--- a/src/Pure/envir.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/envir.ML Fri Sep 15 22:56:13 2006 +0200
@@ -268,7 +268,7 @@
in subst T end;
(*Substitute for type Vars in a term*)
-val subst_TVars = map_term_types o typ_subst_TVars;
+val subst_TVars = map_types o typ_subst_TVars;
(*Substitute for Vars in a term *)
fun subst_Vars itms t = if Vartab.is_empty itms then t else
--- a/src/Pure/logic.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/logic.ML Fri Sep 15 22:56:13 2006 +0200
@@ -555,7 +555,7 @@
(fn Free (x, T) => Var ((x, 0), T)
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
| t => t)
- |> Term.map_term_types varifyT
+ |> Term.map_types varifyT
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
fun unvarify tm =
@@ -564,7 +564,7 @@
| Var (xi, _) => raise TERM (bad_schematic xi, [tm])
| Free (x, _) => raise TERM (bad_fixed x, [tm])
| t => t)
- |> Term.map_term_types unvarifyT
+ |> Term.map_types unvarifyT
handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
@@ -572,11 +572,11 @@
val legacy_varify =
Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
- Term.map_term_types legacy_varifyT;
+ Term.map_types legacy_varifyT;
val legacy_unvarify =
Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
- Term.map_term_types legacy_unvarifyT;
+ Term.map_types legacy_unvarifyT;
(* goal states *)
--- a/src/Pure/proofterm.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/proofterm.ML Fri Sep 15 22:56:13 2006 +0200
@@ -604,7 +604,7 @@
(case AList.lookup (op =) fmap f of
NONE => TFree f
| SOME b => TVar ((b, 0), S));
- in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
+ in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
end;
@@ -630,7 +630,7 @@
[] => prf (*nothing to do!*)
| _ =>
let val frzT = map_type_tvar (freeze_one alist)
- in map_proof_terms (map_term_types frzT) frzT prf end)
+ in map_proof_terms (map_types frzT) frzT prf end)
end;
end;
--- a/src/Pure/sign.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/sign.ML Fri Sep 15 22:56:13 2006 +0200
@@ -461,7 +461,7 @@
let
val _ = Context.check_thy thy;
val _ = check_vars tm;
- val tm' = Term.map_term_types (certify_typ thy) tm;
+ val tm' = Term.map_types (certify_typ thy) tm;
val T = type_check pp tm';
val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
val tm'' = Consts.certify pp (tsig_of thy) consts tm';
--- a/src/Pure/term.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/term.ML Fri Sep 15 22:56:13 2006 +0200
@@ -68,7 +68,7 @@
val map_aterms: (term -> term) -> term -> term
val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
val map_type_tfree: (string * sort -> typ) -> typ -> typ
- val map_term_types: (typ -> typ) -> term -> term
+ val map_types: (typ -> typ) -> term -> term
val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
@@ -423,7 +423,7 @@
fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
-fun map_term_types f =
+fun map_types f =
let
fun map_aux (Const (a, T)) = Const (a, f T)
| map_aux (Free (a, T)) = Free (a, f T)
@@ -911,7 +911,7 @@
in subst ty end;
fun subst_atomic_types [] tm = tm
- | subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm;
+ | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
fun typ_subst_TVars [] ty = ty
| typ_subst_TVars inst ty =
@@ -922,7 +922,7 @@
in subst ty end;
fun subst_TVars [] tm = tm
- | subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm;
+ | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
fun subst_Vars [] tm = tm
| subst_Vars inst tm =
--- a/src/Pure/thm.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/thm.ML Fri Sep 15 22:56:13 2006 +0200
@@ -1138,7 +1138,7 @@
val ((x, i), S) = Term.dest_TVar T handle TYPE _ =>
raise THM ("unconstrainT: not a type variable", 0, [th]);
val T' = TVar ((x, i), []);
- val unconstrain = Term.map_term_types (Term.map_atyps (fn U => if U = T then T' else U));
+ val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
val constraints = map (curry Logic.mk_inclass T') S;
in
Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
--- a/src/Pure/type.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/type.ML Fri Sep 15 22:56:13 2006 +0200
@@ -238,7 +238,7 @@
(case AList.lookup (op =) fmap f of
NONE => TFree f
| SOME xi => TVar (xi, S));
- in (map_term_types (map_type_tfree thaw) t, fmap) end;
+ in (map_types (map_type_tfree thaw) t, fmap) end;
(* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)
@@ -277,8 +277,8 @@
in
(case alist of
[] => (t, fn x => x) (*nothing to do!*)
- | _ => (map_term_types (map_type_tvar (freeze_one alist)) t,
- map_term_types (map_type_tfree (thaw_one (map swap alist)))))
+ | _ => (map_types (map_type_tvar (freeze_one alist)) t,
+ map_types (map_type_tfree (thaw_one (map swap alist)))))
end;
val freeze = #1 o freeze_thaw;
--- a/src/Pure/unify.ML Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/unify.ML Fri Sep 15 22:56:13 2006 +0200
@@ -636,7 +636,7 @@
Term.map_atyps (fn T as TVar ((x, i), S) =>
if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
val decr_indexes =
- Term.map_term_types decr_indexesT #>
+ Term.map_types decr_indexesT #>
Term.map_aterms (fn t as Var ((x, i), T) =>
if i > maxidx then Var ((x, i - offset), T) else t | t => t);