# HG changeset patch # User wenzelm # Date 1247865100 -7200 # Node ID 8e77b6a250d5f3d78deba6a45fecf5fd7fe3c16a # Parent 70c0bcd0adfbd80560fb80d1232083b5ded8caad tuned/modernized Envir.subst_XXX; diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Library/reflection.ML --- 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 diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Nominal/nominal_inductive.ML --- 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 = diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Nominal/nominal_inductive2.ML --- 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 = diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Tools/Datatype/datatype_case.ML --- 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); diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Tools/Function/context_tree.ML --- 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 diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Tools/Function/fundef_datatype.ML --- 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 diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Tools/Function/pattern_split.ML --- 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], []) diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Tools/TFL/casesplit.ML --- 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 diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Tools/TFL/thry.ML --- 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; diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Tools/inductive.ML --- 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) diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOL/Tools/inductive_set.ML --- 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 = diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/HOLCF/Tools/adm_tac.ML --- 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; diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/Pure/Isar/overloading.ML --- 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') diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/Pure/Proof/extraction.ML --- 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}; diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/Pure/defs.ML --- 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); diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/Pure/pattern.ML --- 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; diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/Pure/proofterm.ML --- 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 diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/Pure/thm.ML --- 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 diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/Tools/Compute_Oracle/linker.ML --- 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 diff -r 70c0bcd0adfb -r 8e77b6a250d5 src/Tools/coherent.ML --- 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)