# HG changeset patch # User wenzelm # Date 1425596457 -3600 # Node ID b60e65ad13df45f6540d10f6733e2c137e55a0de # Parent eb59c6968219fbdcd573c9d5e1021812ba4daf49 tuned -- more explicit use of context; diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- 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; diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/Meson/meson.ML --- 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; diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/Metis/metis_reconstruct.ML --- 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)) diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/Old_Datatype/old_datatype.ML --- 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 = diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/Old_Datatype/old_datatype_aux.ML --- 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); diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- 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, ...} => diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/Quickcheck/random_generators.ML --- 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; diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/SMT/z3_replay_methods.ML --- 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 diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/code_evaluation.ML --- 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; diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/datatype_realizer.ML --- 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)])]) diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/record.ML --- 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 diff -r eb59c6968219 -r b60e65ad13df src/HOL/Tools/reification.ML --- 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;