--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Mar 06 00:00:57 2015 +0100
@@ -213,11 +213,13 @@
fun cterm_instantiate_pos cts thm =
let
- val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+ val thy = Thm.theory_of_thm thm;
val vars = Term.add_vars (Thm.prop_of thm) [];
val vars' = rev (drop (length vars - length cts) vars);
- val ps = map_filter (fn (_, NONE) => NONE
- | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
+ val ps =
+ map_filter
+ (fn (_, NONE) => NONE
+ | (var, SOME ct) => SOME (Thm.cterm_of thy (Var var), ct)) (vars' ~~ cts);
in
Drule.cterm_instantiate ps thm
end;
--- a/src/HOL/Tools/Meson/meson.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Fri Mar 06 00:00:57 2015 +0100
@@ -352,10 +352,10 @@
in
fun freeze_spec th ctxt =
let
- val cert = Proof_Context.cterm_of ctxt;
val ([x], ctxt') =
Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
- val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
+ val spec' = spec
+ |> Thm.instantiate ([], [(spec_var, Proof_Context.cterm_of ctxt' (Free (x, spec_varT)))]);
in (th RS spec', ctxt') end
end;
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Mar 06 00:00:57 2015 +0100
@@ -398,21 +398,19 @@
(case Thm.tpairs_of th of
[] => th
| pairs =>
- let
- val thy = Thm.theory_of_thm th
- val cert = Thm.cterm_of thy
- val certT = Thm.ctyp_of thy
- val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
-
- fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
- fun mk (v, (T, t)) = (cert (Var (v, Envir.subst_type tyenv T)), cert t)
-
- val instsT = Vartab.fold (cons o mkT) tyenv []
- val insts = Vartab.fold (cons o mk) tenv []
- in
- Thm.instantiate (instsT, insts) th
- end
- handle THM _ => th)
+ let
+ val thy = Thm.theory_of_thm th
+ val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
+
+ fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of thy) (TVar (v, S), T)
+ fun mk (v, (T, t)) = apply2 (Thm.cterm_of thy) (Var (v, Envir.subst_type tyenv T), t)
+
+ val instsT = Vartab.fold (cons o mkT) tyenv []
+ val insts = Vartab.fold (cons o mk) tenv []
+ in
+ Thm.instantiate (instsT, insts) th
+ end
+ handle THM _ => th)
fun is_metis_literal_genuine (_, (s, _)) =
not (String.isPrefix class_prefix (Metis_Name.toString s))
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Mar 06 00:00:57 2015 +0100
@@ -609,8 +609,6 @@
val (indrule_lemma_prems, indrule_lemma_concls) =
split_list (map2 mk_indrule_lemma descr' recTs);
- val cert = Thm.cterm_of thy6;
-
val indrule_lemma =
Goal.prove_sorry_global thy6 [] []
(Logic.mk_implies
@@ -627,7 +625,8 @@
val frees =
if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))]
else map (Free o apfst fst o dest_Var) Ps;
- val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
+ val indrule_lemma' =
+ cterm_instantiate (map (Thm.cterm_of thy6) Ps ~~ map (Thm.cterm_of thy6) frees) indrule_lemma;
val dt_induct_prop = Old_Datatype_Prop.make_ind descr;
val dt_induct =
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Fri Mar 06 00:00:57 2015 +0100
@@ -126,7 +126,7 @@
fun ind_tac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
let
- val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
+ val thy = Thm.theory_of_cterm cgoal;
val goal = Thm.term_of cgoal;
val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule));
val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop (Logic.strip_imp_concl goal));
@@ -148,7 +148,8 @@
map_filter (fn (t, u) =>
(case abstr (getP u) of
NONE => NONE
- | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u'))) (ts ~~ ts');
+ | SOME u' =>
+ SOME (apply2 (Thm.cterm_of thy) (t |> getP |> snd |> head_of, u')))) (ts ~~ ts');
val indrule' = cterm_instantiate insts indrule;
in resolve0_tac [indrule'] i end);
@@ -157,7 +158,6 @@
fun exh_tac ctxt exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
let
- val thy = Thm.theory_of_cterm cgoal;
val goal = Thm.term_of cgoal;
val params = Logic.strip_params goal;
val (_, Type (tname, _)) = hd (rev params);
@@ -166,8 +166,8 @@
val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
val exhaustion' =
cterm_instantiate
- [(Thm.cterm_of thy (head_of lhs),
- Thm.cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))]
+ [apply2 (Proof_Context.cterm_of ctxt)
+ (head_of lhs, fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0))]
exhaustion;
in compose_tac ctxt (false, exhaustion', Thm.nprems_of exhaustion) i end);
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Mar 06 00:00:57 2015 +0100
@@ -46,8 +46,7 @@
Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
Var (("P", 0), HOLogic.boolT));
val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
- val cert = Thm.cterm_of thy;
- val insts' = map cert induct_Ps ~~ map cert insts;
+ val insts' = map (Thm.cterm_of thy) induct_Ps ~~ map (Thm.cterm_of thy) insts;
val induct' =
refl RS
(nth (Old_Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i
@@ -204,11 +203,12 @@
Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
absfree ("y", T2) (set_t $ Old_Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
(rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
- val cert = Thm.cterm_of thy1;
val insts =
map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
- val induct' = cterm_instantiate (map cert induct_Ps ~~ map cert insts) induct;
+ val induct' = induct
+ |> cterm_instantiate
+ (map (Thm.cterm_of thy1) induct_Ps ~~ map (Thm.cterm_of thy1) insts);
in
Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
(HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
@@ -379,9 +379,9 @@
fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
let
- val cert = Thm.cterm_of thy;
val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.prems_of exhaustion)));
- val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion;
+ val exhaustion' = exhaustion
+ |> cterm_instantiate [apply2 (Thm.cterm_of thy) (lhs, Free ("x", T))];
fun tac ctxt =
EVERY [resolve_tac ctxt [exhaustion'] 1,
ALLGOALS (asm_simp_tac
@@ -450,10 +450,10 @@
let
val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
- val cert = Thm.cterm_of thy;
val nchotomy' = nchotomy RS spec;
val [v] = Term.add_vars (Thm.concl_of nchotomy') [];
- val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy';
+ val nchotomy'' =
+ cterm_instantiate [apply2 (Thm.cterm_of thy) (Var v, Ma)] nchotomy';
in
Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {context = ctxt, prems, ...} =>
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 06 00:00:57 2015 +0100
@@ -89,24 +89,25 @@
(HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
val Type (_, [_, iT]) = T;
val icT = Thm.ctyp_of thy iT;
- val cert = Thm.cterm_of thy;
val inst = Thm.instantiate_cterm ([(aT, icT)], []);
fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
val t_rhs = lambda t_k proto_t_rhs;
val eqs0 = [subst_v @{term "0::natural"} eq,
subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
- val ((_, (_, eqs2)), lthy') = BNF_LFP_Compat.add_primrec_simple
- [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;
+ val ((_, (_, eqs2)), lthy') = lthy
+ |> BNF_LFP_Compat.add_primrec_simple
+ [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1;
val cT_random_aux = inst pt_random_aux;
val cT_rhs = inst pt_rhs;
val rule = @{thm random_aux_rec}
- |> Drule.instantiate_normalize ([(aT, icT)],
- [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]);
+ |> Drule.instantiate_normalize
+ ([(aT, icT)],
+ [(cT_random_aux, Thm.cterm_of thy t_random_aux), (cT_rhs, Thm.cterm_of thy t_rhs)]);
fun tac ctxt =
ALLGOALS (rtac rule)
THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
- THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2))
+ THEN (ALLGOALS (Proof_Context.fact_tac ctxt eqs2));
val simp = Goal.prove_sorry lthy' [v] [] eq (tac o #context);
in (simp, lthy') end;
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Mar 06 00:00:57 2015 +0100
@@ -108,15 +108,13 @@
fun match_instantiateT ctxt t thm =
if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
- let val certT = Proof_Context.ctyp_of ctxt
- in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
+ Thm.instantiate (gen_certify_inst fst TVar (Proof_Context.ctyp_of ctxt) ctxt thm t, []) thm
else thm
fun match_instantiate ctxt t thm =
- let
- val cert = Proof_Context.cterm_of ctxt
- val thm' = match_instantiateT ctxt t thm
- in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
+ let val thm' = match_instantiateT ctxt t thm in
+ Thm.instantiate ([], gen_certify_inst snd Var (Proof_Context.cterm_of ctxt) ctxt thm' t) thm'
+ end
fun apply_rule ctxt t =
(case Z3_Replay_Rules.apply ctxt (certify_prop ctxt t) of
--- a/src/HOL/Tools/code_evaluation.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/code_evaluation.ML Fri Mar 06 00:00:57 2015 +0100
@@ -204,13 +204,13 @@
fun certify_eval ctxt value conv ct =
let
- val cert = Proof_Context.cterm_of ctxt;
val t = Thm.term_of ct;
val T = fastype_of t;
- val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
+ val mk_eq =
+ Thm.mk_binop (Proof_Context.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT)));
in case value ctxt t
of NONE => Thm.reflexive ct
- | SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
+ | SOME t' => conv ctxt (mk_eq ct (Proof_Context.cterm_of ctxt t')) RS @{thm eq_eq_TrueD}
handle THM _ =>
error ("Failed to certify evaluation result of " ^ Syntax.string_of_term ctxt t)
end;
--- a/src/HOL/Tools/datatype_realizer.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Mar 06 00:00:57 2015 +0100
@@ -27,7 +27,6 @@
fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Old_Datatype_Aux.info) is thy =
let
val ctxt = Proof_Context.init_global thy;
- val cert = Thm.cterm_of thy;
val recTs = Old_Datatype_Aux.get_rec_types descr;
val pnames =
@@ -106,11 +105,11 @@
(map (fn ((((i, _), T), U), tname) =>
make_pred i U T (mk_proj i is r) (Free (tname, T)))
(descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
- val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj
+ val inst = map (apply2 (Thm.cterm_of thy)) (map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
val thm =
- Goal.prove_internal ctxt (map cert prems) (cert concl)
+ Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems) (Thm.cterm_of thy concl)
(fn prems =>
EVERY [
rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
@@ -160,7 +159,6 @@
fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
let
val ctxt = Proof_Context.init_global thy;
- val cert = Thm.cterm_of thy;
val rT = TFree ("'P", @{sort type});
val rT' = TVar (("'P", 0), @{sort type});
@@ -187,11 +185,12 @@
val y' = Free ("y", T);
val thm =
- Goal.prove_internal ctxt (map cert prems)
- (cert (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
+ Goal.prove_internal ctxt (map (Thm.cterm_of thy) prems)
+ (Thm.cterm_of thy
+ (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
(fn prems =>
EVERY [
- rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
+ rtac (cterm_instantiate [apply2 (Thm.cterm_of thy) (y, y')] exhaust) 1,
ALLGOALS (EVERY'
[asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
--- a/src/HOL/Tools/record.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/record.ML Fri Mar 06 00:00:57 2015 +0100
@@ -1460,8 +1460,6 @@
avoid problems with higher order unification.*)
fun try_param_tac ctxt s rule = CSUBGOAL (fn (cgoal, i) =>
let
- val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
-
val g = Thm.term_of cgoal;
val params = Logic.strip_params g;
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
@@ -1475,7 +1473,7 @@
| [x] => (head_of x, false));
val rule'' =
cterm_instantiate
- (map (apply2 cert)
+ (map (apply2 (Proof_Context.cterm_of ctxt))
(case rev params of
[] =>
(case AList.lookup (op =) (Term.add_frees g []) s of
--- a/src/HOL/Tools/reification.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/reification.ML Fri Mar 06 00:00:57 2015 +0100
@@ -48,7 +48,6 @@
let
val Const (fN, _) = th |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
|> fst |> strip_comb |> fst;
- val cert = Proof_Context.cterm_of ctxt;
val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'));
fun add_fterms (t as t1 $ t2) =
@@ -84,7 +83,7 @@
(fn {context, prems, ...} =>
Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym;
val (cong' :: vars') =
- Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs);
+ Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o Proof_Context.cterm_of ctxt'') vs);
val vs' = map (fst o fst o Term.dest_Var o Thm.term_of o Drule.dest_term) vars';
in (vs', cong') end;
@@ -134,8 +133,6 @@
fun decomp_reify da cgns (ct, ctxt) bds =
let
val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
fun tryabsdecomp (ct, ctxt) bds =
(case Thm.term_of ct of
Abs (_, xT, ta) =>
@@ -143,8 +140,8 @@
val ([raw_xn], ctxt') = Variable.variant_fixes ["x"] ctxt;
val (xn, ta) = Syntax_Trans.variant_abs (raw_xn, xT, ta); (* FIXME !? *)
val x = Free (xn, xT);
- val cx = cert x;
- val cta = cert ta;
+ val cx = Proof_Context.cterm_of ctxt' x;
+ val cta = Proof_Context.cterm_of ctxt' ta;
val bds = (case AList.lookup Type.could_unify bds (HOLogic.listT xT) of
NONE => error "tryabsdecomp: Type not found in the Environement"
| SOME (bsT, atsT) => AList.update Type.could_unify (HOLogic.listT xT,
@@ -172,10 +169,12 @@
val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv);
val (fts, its) =
(map (snd o snd) fnvs,
- map (fn ((vn, vi), (tT, t)) => (cert (Var ((vn, vi), tT)), cert t)) invs);
- val ctyenv = map (fn ((vn, vi), (s, ty)) => (certT (TVar((vn, vi), s)), certT ty)) (Vartab.dest tyenv);
+ map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of thy) (Var ((vn, vi), tT), t)) invs);
+ val ctyenv =
+ map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of thy) (TVar ((vn, vi), s), ty))
+ (Vartab.dest tyenv);
in
- ((map cert fts ~~ replicate (length fts) ctxt,
+ ((map (Thm.cterm_of thy) fts ~~ replicate (length fts) ctxt,
apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
end handle Pattern.MATCH => decomp_reify da congs (ct, ctxt) bds))
end;
@@ -196,8 +195,6 @@
val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt;
val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt';
val thy = Proof_Context.theory_of ctxt'';
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
val vsns_map = vss ~~ vsns;
val xns_map = fst (split_list nths) ~~ xns;
val subst = map (fn (nt, xn) => (nt, Var ((xn, 0), fastype_of nt))) xns_map;
@@ -205,15 +202,15 @@
val (tyenv, tmenv) = Pattern.match thy (rhs_P, Thm.term_of ct) (Vartab.empty, Vartab.empty);
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 subst_ty =
+ map (fn (n, (s, t)) => apply2 (Thm.ctyp_of thy) (TVar (n, s), t)) (Vartab.dest tyenv)
val tml = Vartab.dest tmenv;
val (subst_ns, bds) = fold_map
(fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds =>
let
val name = snd (the (AList.lookup (op =) tml xn0));
val (idx, bds) = index_of name bds;
- in ((cert n, idx |> (HOLogic.mk_nat #> cert)), bds) end) subst bds;
+ in (apply2 (Thm.cterm_of thy) (n, idx |> HOLogic.mk_nat), bds) end) subst bds;
val subst_vs =
let
fun h (Const _ $ (vs as Var (_, lT)) $ _, Var (_, T)) =
@@ -222,12 +219,13 @@
val lT' = sbsT lT;
val (bsT, _) = the (AList.lookup Type.could_unify bds lT);
val vsn = the (AList.lookup (op =) vsns_map vs);
- val cvs = cert (fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT')));
- in (cert vs, cvs) end;
+ val vs' = fold_rev (fn x => fn xs => cns $ x $xs) bsT (Free (vsn, lT'));
+ in apply2 (Thm.cterm_of thy) (vs, vs') end;
in map h subst end;
- val cts = map (fn ((vn, vi), (tT, t)) => (cert (Var ((vn, vi), tT)), cert t))
- (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
- (map (fn n => (n, 0)) xns) tml);
+ val cts =
+ map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of thy) (Var ((vn, vi), tT), t))
+ (fold (AList.delete (fn (((a : string), _), (b, _)) => a = b))
+ (map (fn n => (n, 0)) xns) tml);
val substt =
let
val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, []));
@@ -261,15 +259,17 @@
|> fst)) eqs [];
val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl)) fs [];
val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt;
- val cert = Proof_Context.cterm_of ctxt';
val subst =
- the o AList.lookup (op =) (map2 (fn T => fn v => (T, cert (Free (v, T)))) tys vs);
+ the o AList.lookup (op =)
+ (map2 (fn T => fn v => (T, Proof_Context.cterm_of ctxt' (Free (v, T)))) tys vs);
fun prep_eq eq =
let
val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop
|> HOLogic.dest_eq |> fst |> strip_comb;
- val subst = map_filter (fn (v as Var (_, T)) => SOME (cert v, subst T)
- | _ => NONE) vs;
+ val subst =
+ map_filter
+ (fn (v as Var (_, T)) => SOME (Proof_Context.cterm_of ctxt' v, subst T)
+ | _ => NONE) vs;
in Thm.instantiate ([], subst) eq end;
val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs;
val bds = AList.make (K ([], [])) tys;
@@ -285,10 +285,9 @@
| is_list_var _ = false;
val vars = th |> Thm.prop_of |> Logic.dest_equals |> snd
|> strip_comb |> snd |> filter is_list_var;
- val cert = Proof_Context.cterm_of ctxt;
val vs = map (fn v as Var (_, T) =>
(v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
- val th' = Drule.instantiate_normalize ([], (map o apply2) cert vs) th;
+ val th' = Drule.instantiate_normalize ([], map (apply2 (Proof_Context.cterm_of ctxt)) vs) th;
val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th'));
in Thm.transitive th'' th' end;