--- a/src/HOL/Library/reflection.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Library/reflection.ML Fri Jul 17 23:11:40 2009 +0200
@@ -205,8 +205,8 @@
val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
val rhs_P = subst_free subst rhs
val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty)
- val sbst = Envir.subst_vars (tyenv, tmenv)
- val sbsT = Envir.typ_subst_TVars tyenv
+ val sbst = Envir.subst_term (tyenv, tmenv)
+ val sbsT = Envir.subst_type tyenv
val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
(Vartab.dest tyenv)
val tml = Vartab.dest tmenv
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Jul 17 23:11:40 2009 +0200
@@ -342,7 +342,7 @@
val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
(Vartab.empty, Vartab.empty);
val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
- (map (Envir.subst_vars env) vs ~~
+ (map (Envir.subst_term env) vs ~~
map (fold_rev (NominalDatatype.mk_perm [])
(rev pis' @ pis)) params' @ [z])) ihyp;
fun mk_pi th =
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Jul 17 23:11:40 2009 +0200
@@ -147,7 +147,7 @@
let val env = Pattern.first_order_match thy (p, prop_of th)
(Vartab.empty, Vartab.empty)
in Thm.instantiate ([],
- map (Envir.subst_vars env #> cterm_of thy) vs ~~ cts) th
+ map (Envir.subst_term env #> cterm_of thy) vs ~~ cts) th
end;
fun prove_strong_ind s avoids ctxt =
--- a/src/HOL/Tools/Datatype/datatype_case.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Jul 17 23:11:40 2009 +0200
@@ -293,7 +293,7 @@
end;
fun make_case tab ctxt = gen_make_case
- (match_type (ProofContext.theory_of ctxt)) Envir.subst_TVars fastype_of tab ctxt;
+ (match_type (ProofContext.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt;
val make_case_untyped = gen_make_case (K (K Vartab.empty))
(K (Term.map_types (K dummyT))) (K dummyT);
--- a/src/HOL/Tools/Function/context_tree.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML Fri Jul 17 23:11:40 2009 +0200
@@ -116,8 +116,9 @@
val (c, subs) = (concl_of r, prems_of r)
val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
- val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
- val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
+ val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs
+ val inst = map (fn v =>
+ (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c [])
in
(cterm_instantiate inst r, dep, branches)
end
--- a/src/HOL/Tools/Function/fundef_datatype.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML Fri Jul 17 23:11:40 2009 +0200
@@ -102,7 +102,8 @@
fun inst_constrs_of thy (T as Type (name, _)) =
- map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+ map (fn (Cn,CT) =>
+ Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
(the (Datatype.get_constrs thy name))
| inst_constrs_of thy _ = raise Match
--- a/src/HOL/Tools/Function/pattern_split.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML Fri Jul 17 23:11:40 2009 +0200
@@ -39,7 +39,8 @@
(* This is copied from "fundef_datatype.ML" *)
fun inst_constrs_of thy (T as Type (name, _)) =
- map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+ map (fn (Cn,CT) =>
+ Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
(the (Datatype.get_constrs thy name))
| inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
--- a/src/HOL/Tools/TFL/casesplit.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Fri Jul 17 23:11:40 2009 +0200
@@ -129,8 +129,8 @@
| _ => error "not a valid case thm";
val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
(Vartab.dest type_insts);
- val cPv = ctermify (Envir.subst_TVars type_insts Pv);
- val cDv = ctermify (Envir.subst_TVars type_insts Dv);
+ val cPv = ctermify (Envir.subst_term_types type_insts Pv);
+ val cDv = ctermify (Envir.subst_term_types type_insts Dv);
in
(beta_eta_contract
(case_thm
--- a/src/HOL/Tools/TFL/thry.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Tools/TFL/thry.ML Fri Jul 17 23:11:40 2009 +0200
@@ -35,7 +35,7 @@
fun match_term thry pat ob =
let
val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
- fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
+ fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t)
in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
end;
--- a/src/HOL/Tools/inductive.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Jul 17 23:11:40 2009 +0200
@@ -922,7 +922,7 @@
val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
(Vartab.empty, Vartab.empty);
in
- map (Envir.subst_vars tab) vars
+ map (Envir.subst_term tab) vars
end
in
map (mtch o apsnd prop_of) (cases ~~ intros)
--- a/src/HOL/Tools/inductive_set.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Jul 17 23:11:40 2009 +0200
@@ -324,7 +324,7 @@
fun to_pred_proc thy rules t = case lookup_rule thy I rules t of
NONE => NONE
| SOME (lhs, rhs) =>
- SOME (Envir.subst_vars
+ SOME (Envir.subst_term
(Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rhs);
fun to_pred thms ctxt thm =
--- a/src/HOLCF/Tools/adm_tac.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/HOLCF/Tools/adm_tac.ML Fri Jul 17 23:11:40 2009 +0200
@@ -117,8 +117,8 @@
val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye;
val ctye = map (fn (ixn, (S, T)) =>
(ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye');
- val tv = cterm_of thy (Var (("t", j), Envir.typ_subst_TVars tye' tT));
- val Pv = cterm_of thy (Var (("P", j), Envir.typ_subst_TVars tye' PT));
+ val tv = cterm_of thy (Var (("t", j), Envir.subst_type tye' tT));
+ val Pv = cterm_of thy (Var (("P", j), Envir.subst_type tye' PT));
val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
in rule' end;
--- a/src/Pure/Isar/overloading.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/Pure/Isar/overloading.ML Fri Jul 17 23:11:40 2009 +0200
@@ -76,7 +76,7 @@
| _ => I)
| accumulate_improvements _ = I;
val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
- val ts' = (map o map_types) (Envir.typ_subst_TVars improvements) ts;
+ val ts' = (map o map_types) (Envir.subst_type improvements) ts;
fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty)
of SOME (ty', t') =>
if Type.typ_instance tsig (ty, ty')
--- a/src/Pure/Proof/extraction.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Jul 17 23:11:40 2009 +0200
@@ -103,7 +103,7 @@
fun ren t = the_default t (Term.rename_abs tm1 tm t);
val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
- val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
+ val prems' = map (pairself (Envir.subst_term env o inc o ren)) prems;
val env' = Envir.Envir
{maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
tenv = tenv, tyenv = Tenv};
--- a/src/Pure/defs.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/Pure/defs.ML Fri Jul 17 23:11:40 2009 +0200
@@ -46,7 +46,7 @@
handle Type.TUNIFY => true);
fun match_args (Ts, Us) =
- Option.map Envir.typ_subst_TVars
+ Option.map Envir.subst_type
(SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
--- a/src/Pure/pattern.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/Pure/pattern.ML Fri Jul 17 23:11:40 2009 +0200
@@ -354,7 +354,7 @@
Abs(ns,Ts,ts) =>
(case obj of
Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env
- | _ => let val Tt = Envir.typ_subst_TVars iTs Ts
+ | _ => let val Tt = Envir.subst_type iTs Ts
in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end)
| _ => (case obj of
Abs(nt,Tt,tt) =>
@@ -428,7 +428,7 @@
fun match_rew thy tm (tm1, tm2) =
let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
- SOME (Envir.subst_vars (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
+ SOME (Envir.subst_term (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
handle MATCH => NONE
end;
--- a/src/Pure/proofterm.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/Pure/proofterm.ML Fri Jul 17 23:11:40 2009 +0200
@@ -1087,7 +1087,7 @@
fun prf_subst (pinst, (tyinsts, insts)) =
let
- val substT = Envir.typ_subst_TVars tyinsts;
+ val substT = Envir.subst_type tyinsts;
fun subst' lev (t as Var (ixn, _)) = (case AList.lookup (op =) insts ixn of
NONE => t
--- a/src/Pure/thm.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/Pure/thm.ML Fri Jul 17 23:11:40 2009 +0200
@@ -317,7 +317,7 @@
(Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts},
Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts});
fun mk_ctinst ((x, i), (T, t)) =
- let val T = Envir.typ_subst_TVars Tinsts T in
+ let val T = Envir.subst_type Tinsts T in
(Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy,
maxidx = i, sorts = sorts},
Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts})
@@ -1467,7 +1467,7 @@
fun norm_term_skip env 0 t = Envir.norm_term env t
| norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
let
- val T' = Envir.typ_subst_TVars (Envir.type_env env) T
+ val T' = Envir.subst_type (Envir.type_env env) T
(*Must instantiate types of parameters because they are flattened;
this could be a NEW parameter*)
in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
--- a/src/Tools/Compute_Oracle/linker.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/Tools/Compute_Oracle/linker.ML Fri Jul 17 23:11:40 2009 +0200
@@ -341,7 +341,7 @@
let
val (newsubsts, instances) = Linker.add_instances thy instances monocs
val _ = if not (null newsubsts) then changed := true else ()
- val newpats = map (fn subst => Envir.subst_TVars subst p) newsubsts
+ val newpats = map (fn subst => Envir.subst_term_types subst p) newsubsts
in
PolyPattern (p, instances, instancepats@newpats)
end
--- a/src/Tools/coherent.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/Tools/coherent.ML Fri Jul 17 23:11:40 2009 +0200
@@ -131,7 +131,7 @@
let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
let val cs' = map (fn (Ts, ts) =>
- (map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs
+ (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
in
inst_extra_vars ctxt dom cs' |>
Seq.map_filter (fn (inst, cs'') =>
@@ -184,7 +184,7 @@
(Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
(Vartab.dest tye),
map (fn (ixn, (T, t)) =>
- (Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)),
+ (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
Thm.cterm_of thy t)) (Vartab.dest env) @
map (fn (ixnT, t) =>
(Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)