# HG changeset patch # User wenzelm # Date 1631278759 -7200 # Node ID c2ee8d993d6a46dcdd46a6af1d9fd9885820dd6b # Parent 7829d6435c6087b8dd8b76096ffcc57877ee16d7 clarified signature: more scalable operations; diff -r 7829d6435c60 -r c2ee8d993d6a src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Doc/Implementation/Logic.thy Fri Sep 10 14:59:19 2021 +0200 @@ -586,8 +586,7 @@ @{define_ML Thm.implies_intr: "cterm -> thm -> thm"} \\ @{define_ML Thm.implies_elim: "thm -> thm -> thm"} \\ @{define_ML Thm.generalize: "Names.set * Names.set -> int -> thm -> thm"} \\ - @{define_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list - -> thm -> thm"} \\ + @{define_ML Thm.instantiate: "ctyp TVars.table * cterm Vars.table -> thm -> thm"} \\ @{define_ML Thm.add_axiom: "Proof.context -> binding * term -> theory -> (string * thm) * theory"} \\ @{define_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Analysis/normarith.ML --- a/src/HOL/Analysis/normarith.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Analysis/normarith.ML Fri Sep 10 14:59:19 2021 +0200 @@ -322,7 +322,8 @@ (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests) in fst (RealArith.real_linear_prover translator - (map (fn t => Drule.instantiate_normalize ([(tv_n, Thm.ctyp_of_cterm t)],[]) pth_zero) + (map (fn t => + Drule.instantiate_normalize (TVars.make [(tv_n, Thm.ctyp_of_cterm t)], Vars.empty) pth_zero) zerodests, map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv arg_conv (arg_conv real_poly_conv))) ges', @@ -365,7 +366,7 @@ val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (Thm.chyps_of th1) val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1]) val cps = map (swap o Thm.dest_equals) (cprems_of th11) - val th12 = Drule.instantiate_normalize ([], map (apfst (dest_Var o Thm.term_of)) cps) th11 + val th12 = Drule.instantiate_normalize (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) cps)) th11 val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12; in hd (Variable.export ctxt' ctxt [th13]) end diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Decision_Procs/approximation.ML --- a/src/HOL/Decision_Procs/approximation.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Decision_Procs/approximation.ML Fri Sep 10 14:59:19 2021 +0200 @@ -75,9 +75,10 @@ |> HOLogic.mk_list \<^typ>\nat\ |> Thm.cterm_of ctxt in - (resolve_tac ctxt [Thm.instantiate ([], [((("n", 0), \<^typ>\nat\), n), - ((("prec", 0), \<^typ>\nat\), p), - ((("ss", 0), \<^typ>\nat list\), s)]) + (resolve_tac ctxt [Thm.instantiate (TVars.empty, + Vars.make [((("n", 0), \<^typ>\nat\), n), + ((("prec", 0), \<^typ>\nat\), p), + ((("ss", 0), \<^typ>\nat list\), s)]) @{thm approx_form}] i THEN simp_tac (put_simpset (simpset_of \<^context>) ctxt) i) st end @@ -92,9 +93,10 @@ val s = vs |> map lookup_splitting |> hd |> Thm.cterm_of ctxt in - resolve_tac ctxt [Thm.instantiate ([], [((("s", 0), \<^typ>\nat\), s), - ((("t", 0), \<^typ>\nat\), t), - ((("prec", 0), \<^typ>\nat\), p)]) + resolve_tac ctxt [Thm.instantiate (TVars.empty, + Vars.make [((("s", 0), \<^typ>\nat\), s), + ((("t", 0), \<^typ>\nat\), t), + ((("prec", 0), \<^typ>\nat\), p)]) @{thm approx_tse_form}] i st end end diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Sep 10 14:59:19 2021 +0200 @@ -68,8 +68,8 @@ fun fw mi th th' th'' = let val th0 = if mi then - Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th - else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th + Drule.instantiate_normalize (TVars.empty, Vars.make [(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th + else Drule.instantiate_normalize (TVars.empty, Vars.make [(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th in Thm.implies_elim (Thm.implies_elim th0 th') th'' end in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') @@ -115,11 +115,11 @@ val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt, pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt, - nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi + nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) nmi val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt, - npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi + npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) npi val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, - ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld + ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) ld fun decomp_mpinf fm = case Thm.term_of fm of diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Decision_Procs/ferrante_rackoff_data.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Fri Sep 10 14:59:19 2021 +0200 @@ -73,7 +73,7 @@ let fun h instT = let - val substT = Thm.instantiate (instT, []); + val substT = Thm.instantiate (instT, Vars.empty); val substT_cterm = Drule.cterm_rule substT; val minf' = map substT minf diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Decision_Procs/langford_data.ML --- a/src/HOL/Decision_Procs/langford_data.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Decision_Procs/langford_data.ML Fri Sep 10 14:59:19 2021 +0200 @@ -50,7 +50,7 @@ let fun h instT = let - val substT = Thm.instantiate (instT, []); + val substT = Thm.instantiate (instT, Vars.empty); val substT_cterm = Drule.cterm_rule substT; val qe_bnds' = substT qe_bnds; diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Eisbach/eisbach_rule_insts.ML --- a/src/HOL/Eisbach/eisbach_rule_insts.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Fri Sep 10 14:59:19 2021 +0200 @@ -69,7 +69,7 @@ val (instT, inst) = fold add_inst insts ([], []); in - (Thm.instantiate (instT, []) thm + (Thm.instantiate (TVars.make instT, Vars.empty) thm |> infer_instantiate ctxt inst COMP_INCR asm_rl) |> Thm.adjust_maxidx_thm ~1 diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Eisbach/match_method.ML Fri Sep 10 14:59:19 2021 +0200 @@ -431,7 +431,7 @@ val (prem_ids, ctxt') = context |> add_focus_params params - |> add_focus_schematics (snd schematics) + |> add_focus_schematics (Vars.dest (snd schematics)) |> fold_map add_focus_prem (rev prems) in @@ -455,10 +455,10 @@ val schematic_terms = Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt'' t)) inst []; - val goal'' = Thm.instantiate ([], schematic_terms) goal'; - val concl' = Thm.instantiate_cterm ([], schematic_terms) concl; + val goal'' = Thm.instantiate (TVars.empty, Vars.make schematic_terms) goal'; + val concl' = Thm.instantiate_cterm (TVars.empty, Vars.make schematic_terms) concl; val (schematic_types, schematic_terms') = schematics; - val schematics' = (schematic_types, schematic_terms @ schematic_terms'); + val schematics' = (schematic_types, fold Vars.add schematic_terms schematic_terms'); in ({context = ctxt'', concl = concl', params = params, prems = prems, schematics = schematics', asms = asms} : Subgoal.focus, goal'') diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Import/import_rule.ML Fri Sep 10 14:59:19 2021 +0200 @@ -162,7 +162,7 @@ val tvars = Term.add_tvars (Thm.prop_of thm) [] val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars in - Thm.instantiate ((tvars ~~ map (Thm.global_ctyp_of thy) tfrees), []) thm + Thm.instantiate (TVars.make (tvars ~~ map (Thm.global_ctyp_of thy) tfrees), Vars.empty) thm end fun def' constname rhs thy = @@ -274,7 +274,7 @@ | NONE => (iS, Thm.global_ctyp_of thy (TFree bef)))) tys_before tys_after in - Thm.instantiate (tyinst,[]) th1 + Thm.instantiate (TVars.make tyinst, Vars.empty) th1 end fun inst sigma th = @@ -338,7 +338,7 @@ val tns = map (fn (_, _) => "'") tvs val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt)) val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs)) - val thm' = Thm.instantiate ((tvs ~~ map (Thm.ctyp_of ctxt) vs), []) thm + val thm' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) thm in snd (Global_Theory.add_thm ((binding, thm'), []) thy) end diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Library/Sum_of_Squares/positivstellensatz.ML --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Fri Sep 10 14:59:19 2021 +0200 @@ -476,7 +476,7 @@ fun real_not_eq_conv ct = let val (l,r) = dest_eq (Thm.dest_arg ct) - val th = Thm.instantiate ([],[((("x", 0), \<^typ>\real\),l),((("y", 0), \<^typ>\real\),r)]) neq_th + val th = Thm.instantiate (TVars.empty, Vars.make [((("x", 0), \<^typ>\real\),l),((("y", 0), \<^typ>\real\),r)]) neq_th val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th))) val th_x = Drule.arg_cong_rule \<^cterm>\uminus :: real \ _\ th_p val th_n = fconv_rule (arg_conv poly_neg_conv) th_x @@ -740,16 +740,16 @@ val elim_abs = eliminate_construct is_abs (fn p => fn ax => - Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax)]) pth_abs) + Thm.instantiate (TVars.empty, Vars.make [(p_v,p), (x_v, Thm.dest_arg ax)]) pth_abs) val elim_max = eliminate_construct is_max (fn p => fn ax => let val (ax,y) = Thm.dest_comb ax - in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)]) + in Thm.instantiate (TVars.empty, Vars.make [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)]) pth_max end) val elim_min = eliminate_construct is_min (fn p => fn ax => let val (ax,y) = Thm.dest_comb ax - in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)]) + in Thm.instantiate (TVars.empty, Vars.make [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)]) pth_min end) in first_conv [elim_abs, elim_max, elim_min, all_conv] end; diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Library/cconv.ML --- a/src/HOL/Library/cconv.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Library/cconv.ML Fri Sep 10 14:59:19 2021 +0200 @@ -183,7 +183,8 @@ ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct | _ => cv ct) -fun inst_imp_cong ct = Thm.instantiate ([], [((("A", 0), propT), ct)]) Drule.imp_cong +fun inst_imp_cong ct = + Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), ct)]) Drule.imp_cong (*rewrite B in A1 \ ... \ An \ B*) fun concl_cconv 0 cv ct = cv ct @@ -203,10 +204,12 @@ NONE => (As, B) | SOME (A,B) => strip_prems (i - 1) (A::As) B val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n [] - val rewr_imp_concl = Thm.instantiate ([], [((("C", 0), propT), concl)]) @{thm rewr_imp} + val rewr_imp_concl = + Thm.instantiate (TVars.empty, Vars.make [((("C", 0), propT), concl)]) @{thm rewr_imp} val th1 = cv prem RS rewr_imp_concl val nprems = Thm.nprems_of th1 - fun inst_cut_rl ct = Thm.instantiate ([], [((("psi", 0), propT), ct)]) cut_rl + fun inst_cut_rl ct = + Thm.instantiate (TVars.empty, Vars.make [((("psi", 0), propT), ct)]) cut_rl fun f p th = (th RS inst_cut_rl p) |> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq})) in fold f prems th1 end diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Library/old_recdef.ML --- a/src/HOL/Library/old_recdef.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Library/old_recdef.ML Fri Sep 10 14:59:19 2021 +0200 @@ -305,8 +305,8 @@ in Conv.fconv_rule Drule.beta_eta_conversion (case_thm - |> Thm.instantiate (type_cinsts, []) - |> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)])) + |> Thm.instantiate (TVars.make type_cinsts, Vars.empty) + |> Thm.instantiate (TVars.empty, Vars.make [(Pv, abs_ct), (Dv, free_ct)])) end; @@ -1121,7 +1121,8 @@ val gspec = Thm.forall_intr (Thm.cterm_of \<^context> x) spec in fun SPEC tm thm = - let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec + let val gspec' = + Drule.instantiate_normalize (TVars.make [(TV, Thm.ctyp_of_cterm tm)], Vars.empty) gspec in thm RS (Thm.forall_elim tm gspec') end end; @@ -1140,8 +1141,8 @@ let val ctm2 = Thm.cterm_of ctxt tm2 in ((i, Thm.typ_of_cterm ctm2), ctm2) end) fun certify ctxt (ty_theta,tm_theta) = - (cty_theta ctxt (Vartab.dest ty_theta), - ctm_theta ctxt (Vartab.dest tm_theta)) + (TVars.make (cty_theta ctxt (Vartab.dest ty_theta)), + Vars.make (ctm_theta ctxt (Vartab.dest tm_theta))) in fun GEN ctxt v th = let val gth = Thm.forall_intr v th diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Library/rewrite.ML --- a/src/HOL/Library/rewrite.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Library/rewrite.ML Fri Sep 10 14:59:19 2021 +0200 @@ -272,7 +272,7 @@ ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x)))) val tyinsts = Term.add_tvars prop [] |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x)))) - in Drule.instantiate_normalize (tyinsts, insts) thm end + in Drule.instantiate_normalize (TVars.make tyinsts, Vars.make insts) thm end fun unify_with_rhs context to env thm = let diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Matrix_LP/Compute_Oracle/linker.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Fri Sep 10 14:59:19 2021 +0200 @@ -326,7 +326,7 @@ let val (newsubsts, instances) = Linker.add_instances thy instances monocs val _ = if not (null newsubsts) then changed := true else () - val newths = map (fn subst => Thm.instantiate (conv_subst thy subst, []) th) newsubsts + val newths = map (fn subst => Thm.instantiate (TVars.make (conv_subst thy subst), Vars.empty) th) newsubsts (* val _ = if not (null newths) then (print ("added new theorems: ", newths); ()) else ()*) val newmonos = fold (fn th => fn monos => (snd (collect_consts_of_thm th))@monos) newths [] in diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Sep 10 14:59:19 2021 +0200 @@ -1397,8 +1397,8 @@ REPEAT (TRY (resolve_tac context [conjI] 1) THEN asm_full_simp_tac ind_ss5 1)] end); - val induct_aux' = Thm.instantiate ([], - map (fn (s, Var (v as (_, T))) => + val induct_aux' = Thm.instantiate (TVars.empty, + Vars.make (map (fn (s, Var (v as (_, T))) => (v, Thm.global_cterm_of thy9 (Free (s, T)))) (pnames ~~ map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct_aux)))) @ @@ -1406,7 +1406,7 @@ let val f' = Logic.varify_global f in (dest_Var f', Thm.global_cterm_of thy9 (Const (\<^const_name>\Nominal.supp\, fastype_of f'))) - end) fresh_fs) induct_aux; + end) fresh_fs)) induct_aux; val induct = Goal.prove_global_future thy9 [] (map (augment_sort thy9 fs_cp_sort) ind_prems) @@ -1571,8 +1571,8 @@ (augment_sort thy1 pt_cp_sort (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P))) (fn {context = ctxt, ...} => - dresolve_tac ctxt [Thm.instantiate ([], - [((("pi", 0), permT), + dresolve_tac ctxt [Thm.instantiate (TVars.empty, + Vars.make [((("pi", 0), permT), Thm.global_cterm_of thy11 (Const (\<^const_name>\rev\, permT --> permT) $ pi))]) th] 1 THEN NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths) in (ths, ths') end) dt_atomTs); @@ -1662,8 +1662,8 @@ resolve_tac ctxt [unique] 1, SUBPROOF (fn {context = ctxt', prems = prems', params = [(_, a), (_, b)], ...} => EVERY [cut_facts_tac [rec_prem] 1, - resolve_tac ctxt' [Thm.instantiate ([], - [((("pi", 0), mk_permT aT), + resolve_tac ctxt' [Thm.instantiate (TVars.empty, + Vars.make [((("pi", 0), mk_permT aT), Thm.cterm_of ctxt' (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th] 1, asm_simp_tac (put_simpset HOL_ss ctxt' addsimps @@ -1882,8 +1882,8 @@ val U as Type (_, [Type (_, [T, _])]) = fastype_of p; val l = find_index (equal T) dt_atomTs; val th = nth (nth rec_equiv_thms' l) k; - val th' = Thm.instantiate ([], - [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th; + val th' = Thm.instantiate (TVars.empty, + Vars.make [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th; in resolve_tac ctxt [th'] 1 end; val th' = Goal.prove context'' [] [] (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y)) diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Fri Sep 10 14:59:19 2021 +0200 @@ -33,8 +33,8 @@ fun res_inst_tac_term ctxt = gen_res_inst_tac_term ctxt (fn instT => fn inst => Thm.instantiate - (map (apfst dest_TVar) instT, - map (apfst dest_Var) inst)); + (TVars.make (map (apfst dest_TVar) instT), + Vars.make (map (apfst dest_Var) inst))); fun res_inst_tac_term' ctxt = gen_res_inst_tac_term ctxt @@ -152,8 +152,8 @@ in case subtract (op =) vars vars' of [Var v] => Seq.single - (Thm.instantiate ([], - [(v, Thm.cterm_of ctxt (fold_rev Term.abs params (Bound 0)))]) st) + (Thm.instantiate (TVars.empty, + Vars.make [(v, Thm.cterm_of ctxt (fold_rev Term.abs params (Bound 0)))]) st) | _ => error "fresh_fun_simp: Too many variables, please report." end in diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Sep 10 14:59:19 2021 +0200 @@ -343,11 +343,11 @@ val pis'' = fold (concat_perm #> map) pis' pis; val env = Pattern.first_order_match thy (ihypt, Thm.prop_of ihyp) (Vartab.empty, Vartab.empty); - val ihyp' = Thm.instantiate ([], - map (fn (v, t) => (dest_Var v, Thm.global_cterm_of thy t)) + val ihyp' = Thm.instantiate (TVars.empty, + Vars.make (map (fn (v, t) => (dest_Var v, Thm.global_cterm_of thy t)) (map (Envir.subst_term env) vs ~~ map (fold_rev (NominalDatatype.mk_perm []) - (rev pis' @ pis)) params' @ [z])) ihyp; + (rev pis' @ pis)) params' @ [z]))) ihyp; fun mk_pi th = Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}] addsimprocs [NominalDatatype.perm_simproc]) diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Sep 10 14:59:19 2021 +0200 @@ -149,7 +149,9 @@ fun inst_params thy (vs, p) th cts = let val env = Pattern.first_order_match thy (p, Thm.prop_of th) (Vartab.empty, Vartab.empty) - in Thm.instantiate ([], map (dest_Var o Envir.subst_term env) vs ~~ cts) th end; + in + Thm.instantiate (TVars.empty, Vars.make (map (dest_Var o Envir.subst_term env) vs ~~ cts)) th + end; fun prove_strong_ind s alt_name avoids ctxt = let diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Real_Asymp/multiseries_expansion.ML --- a/src/HOL/Real_Asymp/multiseries_expansion.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Real_Asymp/multiseries_expansion.ML Fri Sep 10 14:59:19 2021 +0200 @@ -219,10 +219,10 @@ case tvs of [v] => let - val thm' = Thm.instantiate ([(v, Thm.ctyp_of_cterm ct)], []) thm + val thm' = Thm.instantiate (TVars.make [(v, Thm.ctyp_of_cterm ct)], Vars.empty) thm val vs = take (length cts) (rev (Term.add_vars (Thm.concl_of thm') [])) in - Thm.instantiate ([], vs ~~ cts) thm' + Thm.instantiate (TVars.empty, Vars.make (vs ~~ cts)) thm' end | _ => raise THM ("get_parity", 0, [thm]) end diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Fri Sep 10 14:59:19 2021 +0200 @@ -97,8 +97,8 @@ val insts' = map (apfst mapT_and_recertify) insts; in Thm.instantiate - (map (apfst (dest_TVar o Thm.typ_of)) instTs, - map (apfst (dest_Var o Thm.term_of)) insts') + (TVars.make (map (apfst (dest_TVar o Thm.typ_of)) instTs), + Vars.make (map (apfst (dest_Var o Thm.term_of)) insts')) end; fun tvar_clash ixn S S' = @@ -152,7 +152,7 @@ map (fn (v, (S, U)) => ((v, S), Thm.ctyp_of ctxt U)) tyinsts; val insts' = map (fn (idxn, ct) => ((idxn, Thm.typ_of_cterm ct), ct)) insts; - val rule' = Thm.instantiate (tyinsts', insts') rule; + val rule' = Thm.instantiate (TVars.make tyinsts', Vars.make insts') rule; in fold Thm.elim_implies prems rule' end; local @@ -299,8 +299,8 @@ val [alphaI] = #2 (dest_Type T); in Thm.instantiate - ([(alpha, Thm.ctyp_of ctxt alphaI)], - [((v, treeT alphaI), ct')]) @{thm subtract_Tip} + (TVars.make [(alpha, Thm.ctyp_of ctxt alphaI)], + Vars.make [((v, treeT alphaI), ct')]) @{thm subtract_Tip} end | subtractProver ctxt (Const (\<^const_name>\Node\, nT) $ l $ x $ d $ r) ct dist_thm = let diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Sep 10 14:59:19 2021 +0200 @@ -579,7 +579,7 @@ map (apfst (dest_Var o type_devar typeval_env)) term_pairing |> map (apsnd (Thm.cterm_of ctxt)) in - Thm.instantiate (typeval, termval) scheme_thm + Thm.instantiate (TVars.make typeval, Vars.make termval) scheme_thm end (*FIXME this is bad form?*) diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Sep 10 14:59:19 2021 +0200 @@ -943,7 +943,7 @@ end fun instantiate_tac from to = - PRIMITIVE (Thm.instantiate ([], [(from, to)])) + PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(from, to)])) val tactic = if is_none var_opt then no_tac diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Argo/argo_real.ML --- a/src/HOL/Tools/Argo/argo_real.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Argo/argo_real.ML Fri Sep 10 14:59:19 2021 +0200 @@ -207,8 +207,10 @@ | var_of_add_cmp t = raise TERM ("var_of_add_cmp", [t]) fun add_cmp_conv ctxt n thm = - let val v = var_of_add_cmp (Thm.prop_of thm) - in Conv.rewr_conv (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (mk_number n))]) thm) end + let val v = var_of_add_cmp (Thm.prop_of thm) in + Conv.rewr_conv + (Thm.instantiate (TVars.empty, Vars.make [(v, Thm.cterm_of ctxt (mk_number n))]) thm) + end fun mul_cmp_conv ctxt n pos_thm neg_thm = let val thm = if @0 < n then pos_thm else neg_thm diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Argo/argo_tactic.ML --- a/src/HOL/Tools/Argo/argo_tactic.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Argo/argo_tactic.ML Fri Sep 10 14:59:19 2021 +0200 @@ -305,7 +305,8 @@ let val cprop = as_prop ct in Thm.implies_intr cprop (f (Thm.assume cprop)) end -fun instantiate cv ct = Thm.instantiate ([], [(Term.dest_Var (Thm.term_of cv), ct)]) +fun instantiate cv ct = + Thm.instantiate (TVars.empty, Vars.make [(Term.dest_Var (Thm.term_of cv), ct)]) (* proof replay for tautologies *) diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 10 14:59:19 2021 +0200 @@ -2060,7 +2060,7 @@ val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)}; in - Thm.instantiate ([], insts) coind + Thm.instantiate (TVars.empty, Vars.make insts) coind |> unfold_thms ctxt unfolds end; diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 10 14:59:19 2021 +0200 @@ -716,7 +716,7 @@ fun inst_thm t thm = Thm.instantiate' [] [SOME (Thm.cterm_of lthy t)] - (Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm)); + (Thm.instantiate (TVars.make rho_As, Vars.empty) (Drule.zero_var_indexes thm)); val uexhaust_thm = inst_thm u exhaust_thm; diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Fri Sep 10 14:59:19 2021 +0200 @@ -210,7 +210,7 @@ THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 THEN CONVERSION (split_params_conv ctxt then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3) - |> Thm.instantiate ([], [(P_var, P_inst), (x_var, x_inst)]) + |> Thm.instantiate (TVars.empty, Vars.make [(P_var, P_inst), (x_var, x_inst)]) |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt) |> singleton (Variable.export ctxt' ctxt) in diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Function/relation.ML --- a/src/HOL/Tools/Function/relation.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Function/relation.ML Fri Sep 10 14:59:19 2021 +0200 @@ -18,7 +18,8 @@ fun inst_state_tac ctxt inst = SUBGOAL (fn (goal, _) => (case Term.add_vars goal [] of - [v as (_, T)] => PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (inst T))])) + [v as (_, T)] => + PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(v, Thm.cterm_of ctxt (inst T))])) | _ => no_tac)); fun relation_tac ctxt rel i = @@ -38,7 +39,7 @@ |> map_types Type_Infer.paramify_vars |> Type.constraint T |> Syntax.check_term ctxt; - in PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt rel')])) end + in PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(v, Thm.cterm_of ctxt rel')])) end | _ => no_tac)); fun relation_infer_tac ctxt rel i = diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Lifting/lifting_bnf.ML --- a/src/HOL/Tools/Lifting/lifting_bnf.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Sep 10 14:59:19 2021 +0200 @@ -24,7 +24,7 @@ val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd)) val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars val inst = map dest_Var vars ~~ map (Thm.cterm_of ctxt) UNIVs - val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst) + val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize (TVars.empty, Vars.make inst) |> Local_Defs.unfold0 ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)} |> (fn thm => thm RS sym) val rel_mono = rel_mono_of_bnf bnf diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Sep 10 14:59:19 2021 +0200 @@ -119,7 +119,7 @@ val instT = Vartab.fold (fn (a, (S, T)) => cons ((a, S), Thm.ctyp_of ctxt T)) (mk_inst_of_lift_def qty lift_def) [] - val phi = Morphism.instantiate_morphism (instT, []) + val phi = Morphism.instantiate_morphism (TVars.make instT, Vars.empty) in morph_lift_def phi lift_def end diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Fri Sep 10 14:59:19 2021 +0200 @@ -285,7 +285,7 @@ val match_env = Sign.typ_match (Proof_Context.theory_of ctxt) (qty_schematic, qty) Vartab.empty fun prep_ty (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty) val ty_inst = Vartab.fold (cons o prep_ty) match_env [] - in Thm.instantiate (ty_inst, []) quot_thm end + in Thm.instantiate (TVars.make ty_inst, Vars.empty) quot_thm end fun check_rty_type ctxt rty quot_thm = let diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Fri Sep 10 14:59:19 2021 +0200 @@ -358,7 +358,8 @@ val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt; val spec' = spec - |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]); + |> Thm.instantiate + (TVars.empty, Vars.make [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]); in (th RS spec', ctxt') end end; diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 10 14:59:19 2021 +0200 @@ -42,9 +42,9 @@ fun transform_elim_theorem th = (case Thm.concl_of th of (*conclusion variable*) \<^const>\Trueprop\ $ (Var (v as (_, \<^typ>\bool\))) => - Thm.instantiate ([], [(v, cfalse)]) th + Thm.instantiate (TVars.empty, Vars.make [(v, cfalse)]) th | Var (v as (_, \<^typ>\prop\)) => - Thm.instantiate ([], [(v, ctp_false)]) th + Thm.instantiate (TVars.empty, Vars.make [(v, ctp_false)]) th | _ => th) @@ -370,7 +370,8 @@ th ctxt1 val (cnf_ths, ctxt2) = clausify nnf_th fun intr_imp ct th = - Thm.instantiate ([], [((("i", 0), \<^typ>\nat\), Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))]) + Thm.instantiate (TVars.empty, + Vars.make [((("i", 0), \<^typ>\nat\), Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))]) (zero_var_indexes @{thm skolem_COMBK_D}) RS Thm.implies_intr ct th in diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 10 14:59:19 2021 +0200 @@ -103,7 +103,7 @@ fun inst_excluded_middle i_atom = @{lemma "P \ \ P \ False" by (rule notE)} - |> instantiate_normalize ([], [((("P", 0), \<^typ>\bool\), i_atom)]) + |> instantiate_normalize (TVars.empty, Vars.make [((("P", 0), \<^typ>\bool\), i_atom)]) fun assume_inference ctxt type_enc concealed sym_tab atom = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom) @@ -174,7 +174,7 @@ val tvs = Term.add_tvars (Thm.full_prop_of th) [] fun inc_tvar ((a, i), s) = (((a, i), s), Thm.ctyp_of ctxt (TVar ((a, i + inc), s))) in - Thm.instantiate (map inc_tvar tvs, []) th + Thm.instantiate (TVars.make (map inc_tvar tvs), Vars.empty) th end (*Like RSN, but we rename apart only the type variables. Vars here typically @@ -217,7 +217,7 @@ again. We could do this the first time around but this error occurs seldom and we don't want to break existing proofs in subtle ways or slow them down.*) if null ps then raise TERM z - else res (apply2 (Drule.instantiate_normalize (ps, [])) (th1', th2)) + else res (apply2 (Drule.instantiate_normalize (TVars.make ps, Vars.empty)) (th1', th2)) end end @@ -407,7 +407,7 @@ val instsT = Vartab.fold (cons o mkT) tyenv [] val insts = Vartab.fold (cons o mk) tenv [] in - Thm.instantiate (instsT, insts) th + Thm.instantiate (TVars.make instsT, Vars.make insts) th end handle THM _ => th) @@ -574,7 +574,8 @@ tyenv [] val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')] in - Drule.instantiate_normalize (ty_inst, map (apfst (dest_Var o Thm.term_of)) t_inst) th + Drule.instantiate_normalize + (TVars.make ty_inst, Vars.make (map (apfst (dest_Var o Thm.term_of)) t_inst)) th end | _ => raise Fail "expected a single non-zapped, non-Metis Var") in diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Sep 10 14:59:19 2021 +0200 @@ -240,10 +240,11 @@ map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (Thm.prems_of case_th)) val case_th' = - Thm.instantiate ([], inst_of_matches pats) case_th + Thm.instantiate (TVars.empty, Vars.make (inst_of_matches pats)) case_th OF replicate nargs @{thm refl} val thesis = - Thm.instantiate ([], inst_of_matches (Thm.prems_of case_th' ~~ map Thm.prop_of prems2)) + Thm.instantiate (TVars.empty, + Vars.make (inst_of_matches (Thm.prems_of case_th' ~~ map Thm.prop_of prems2))) case_th' OF prems2 in resolve_tac ctxt2 [thesis] 1 end in diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 10 14:59:19 2021 +0200 @@ -871,7 +871,7 @@ fun rewrite_pat (ct1, ct2) = (ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2))) val t_insts' = map rewrite_pat (Vars.dest t_insts) - val intro'' = Thm.instantiate (TVars.dest T_insts, t_insts') intro + val intro'' = Thm.instantiate (T_insts, Vars.make t_insts') intro val [intro'''] = Variable.export ctxt3 ctxt [intro''] val intro'''' = Simplifier.full_simplify @@ -941,9 +941,9 @@ val f' = absdummy (U --> T') (Bound 0 $ y) val th' = Thm.instantiate - ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')), + (TVars.make [(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')), (dest_TVar uninst_T', Thm.ctyp_of ctxt' T')], - [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th + Vars.make [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th'] in th' @@ -1083,13 +1083,16 @@ val instT = TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) (subst_of (pred', pred)) []; - in Thm.instantiate (instT, []) th end + in Thm.instantiate (TVars.make instT, Vars.empty) th end fun instantiate_ho_args th = let val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th val ho_args' = map dest_Var (ho_args_of_typ T args') - in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end + in + Thm.instantiate (TVars.empty, Vars.make (ho_args' ~~ map (Thm.cterm_of ctxt') ho_args)) + th + end val outp_pred = Term_Subst.instantiate (subst_of (inp_pred, pred), Vars.empty) inp_pred val ((_, ths'), ctxt1) = diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri Sep 10 14:59:19 2021 +0200 @@ -160,10 +160,13 @@ [(th_1,th_2,th_3), (th_1',th_2',th_3')] = let val (mp', mq') = (get_pmi th_1, get_pmi th_1') - val mi_th = FWD (Drule.instantiate_normalize ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1) - [th_1, th_1'] - val infD_th = FWD (Drule.instantiate_normalize ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3'] - val set_th = FWD (Drule.instantiate_normalize ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2'] + val mi_th = + FWD (Drule.instantiate_normalize + (TVars.empty, Vars.make [(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1) [th_1, th_1'] + val infD_th = + FWD (Drule.instantiate_normalize (TVars.empty, Vars.make [(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3'] + val set_th = + FWD (Drule.instantiate_normalize (TVars.empty, Vars.make [(p_v,p), (q_v,q)]) th2) [th_2, th_2'] in (mi_th, set_th, infD_th) end; @@ -504,16 +507,18 @@ if length (distinct (op aconv) bl) <= length (distinct (op aconv) al) then (bl,b0,decomp_minf, - fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_v,B), (D_v,cd)]) th) dp) + fn B => (map (fn th => + Thm.implies_elim (Thm.instantiate (TVars.empty, Vars.make [(B_v,B), (D_v,cd)]) th) dp) [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@ - (map (Thm.instantiate ([],[(B_v,B), (D_v,cd)])) + (map (Thm.instantiate (TVars.empty, Vars.make [(B_v,B), (D_v,cd)])) [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj, bsetdisj,infDconj, infDdisj]), cpmi) else (al,a0,decomp_pinf,fn A => - (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_v,A), (D_v,cd)]) th) dp) + (map (fn th => + Thm.implies_elim (Thm.instantiate (TVars.empty, Vars.make [(A_v,A), (D_v,cd)]) th) dp) [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@ - (map (Thm.instantiate ([],[(A_v,A), (D_v,cd)])) + (map (Thm.instantiate (TVars.empty, Vars.make [(A_v,A), (D_v,cd)])) [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj, asetdisj,infDconj, infDdisj]),cppi) val cpth = diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Sep 10 14:59:19 2021 +0200 @@ -92,7 +92,7 @@ (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; val Type (_, [_, iT]) = T; val icT = Thm.ctyp_of lthy iT; - val inst = Thm.instantiate_cterm ([(a_v, icT)], []); + val inst = Thm.instantiate_cterm (TVars.make [(a_v, icT)], Vars.empty); 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, @@ -105,8 +105,8 @@ val cT_rhs = inst pt_rhs |> Thm.term_of |> dest_Var; val rule = @{thm random_aux_rec} |> Drule.instantiate_normalize - ([(a_v, icT)], - [(cT_random_aux, Thm.cterm_of lthy' t_random_aux), + (TVars.make [(a_v, icT)], + Vars.make [(cT_random_aux, Thm.cterm_of lthy' t_random_aux), (cT_rhs, Thm.cterm_of lthy' t_rhs)]); fun tac ctxt = ALLGOALS (resolve_tac ctxt [rule]) diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Sep 10 14:59:19 2021 +0200 @@ -81,7 +81,7 @@ fun prep_ty (x, (S, ty)) = ((x, S), Thm.global_ctyp_of thy ty) fun prep_trm (x, (T, t)) = ((x, T), Thm.global_cterm_of thy t) in - (map prep_ty tyenv, map prep_trm tenv) + (TVars.make (map prep_ty tyenv), Vars.make (map prep_trm tenv)) end (* Calculates the instantiations for the lemmas: @@ -476,7 +476,8 @@ then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm) else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm) val thm4 = - Drule.instantiate_normalize ([], [(dest_Var insp, Thm.cterm_of ctxt inst)]) thm3 + Drule.instantiate_normalize + (TVars.empty, Vars.make [(dest_Var insp, Thm.cterm_of ctxt inst)]) thm3 in Conv.rewr_conv thm4 ctrm end diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 10 14:59:19 2021 +0200 @@ -35,7 +35,7 @@ fun inst f ct thm = let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) - in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end + in Thm.instantiate (TVars.empty, Vars.make [(dest_Var (Thm.term_of cv), ct)]) thm end in fun instantiate_elim thm = @@ -203,7 +203,7 @@ let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct val inst = map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)] - in Thm.instantiate ([], inst) trigger_eq end + in Thm.instantiate (TVars.empty, Vars.make inst) trigger_eq end fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = let @@ -402,7 +402,7 @@ let val (q, cts) = fold (add_apps add_int_of_nat [] o Thm.cprop_of) thms (false, []) in if q then (thms, nat_int_thms) - else (thms, map (fn ct => Thm.instantiate ([], [(var, ct)]) int_thm) cts) + else (thms, map (fn ct => Thm.instantiate (TVars.empty, Vars.make [(var, ct)]) int_thm) cts) end val setup_nat_as_int = diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/SMT/smt_replay.ML --- a/src/HOL/Tools/SMT/smt_replay.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/SMT/smt_replay.ML Fri Sep 10 14:59:19 2021 +0200 @@ -96,7 +96,8 @@ fun compose (cvs, f, rule) thm = discharge thm - (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule) + (Thm.instantiate + (TVars.empty, Vars.make (map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm))) rule) (* simpset *) diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/SMT/smt_replay_methods.ML --- a/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Fri Sep 10 14:59:19 2021 +0200 @@ -157,12 +157,12 @@ fun match_instantiateT ctxt t thm = if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then - Thm.instantiate (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t, []) thm + Thm.instantiate (TVars.make (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t), Vars.empty) thm else thm fun match_instantiate ctxt t thm = let val thm' = match_instantiateT ctxt t thm in - Thm.instantiate ([], gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t) thm' + Thm.instantiate (TVars.empty, Vars.make (gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t)) thm' end fun discharge _ [] thm = thm diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/SMT/smt_util.ML --- a/src/HOL/Tools/SMT/smt_util.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/SMT/smt_util.ML Fri Sep 10 14:59:19 2021 +0200 @@ -173,7 +173,8 @@ let val cpat = Thm.global_cterm_of thy (Const (name, Sign.the_const_type thy name)) in (destT (Thm.ctyp_of_cterm cpat), cpat) end -fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct +fun instTs cUs (cTs, ct) = + Thm.instantiate_cterm (TVars.make (map (dest_TVar o Thm.typ_of) cTs ~~ cUs), Vars.empty) ct fun instT cU (cT, ct) = instTs [cU] ([cT], ct) fun instT' ct = instT (Thm.ctyp_of_cterm ct) diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Fri Sep 10 14:59:19 2021 +0200 @@ -576,7 +576,7 @@ in thm |> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx - |> Thm.instantiate (map tinst binsts, map inst binsts) + |> Thm.instantiate (TVars.make (map tinst binsts), Vars.make (map inst binsts)) end fun transfer_rule_of_lhs ctxt t = @@ -597,7 +597,7 @@ in thm |> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx - |> Thm.instantiate (map tinst binsts, map inst binsts) + |> Thm.instantiate (TVars.make (map tinst binsts), Vars.make (map inst binsts)) end fun eq_rules_tac ctxt eq_rules = @@ -701,7 +701,7 @@ rev (Term.add_tvars (Thm.full_prop_of thm1) []) |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S)))) val thm2 = thm1 - |> Thm.instantiate (instT, []) + |> Thm.instantiate (TVars.make instT, Vars.empty) |> Raw_Simplifier.rewrite_rule ctxt pre_simps val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt val rule = transfer_rule_of_lhs ctxt' (HOLogic.dest_Trueprop (Thm.concl_of thm2)) @@ -736,7 +736,7 @@ rev (Term.add_tvars (Thm.full_prop_of thm1) []) |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S)))) val thm2 = thm1 - |> Thm.instantiate (instT, []) + |> Thm.instantiate (TVars.make instT, Vars.empty) |> Raw_Simplifier.rewrite_rule ctxt pre_simps val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt val t = HOLogic.dest_Trueprop (Thm.concl_of thm2) diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/coinduction.ML --- a/src/HOL/Tools/coinduction.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/coinduction.ML Fri Sep 10 14:59:19 2021 +0200 @@ -69,8 +69,8 @@ |> fold Variable.declare_thm (raw_thm :: prems); val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl; val (instT, inst) = Thm.match (thm_concl, concl); - val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT; - val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst; + val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) (TVars.dest instT); + val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) (Vars.dest inst); val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd |> map (subst_atomic_types rhoTs); val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs; diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/hologic.ML Fri Sep 10 14:59:19 2021 +0200 @@ -205,16 +205,16 @@ let val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ) handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]); - val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]); - in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end; + val inst = (TVars.empty, Vars.make [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]); + in Drule.implies_elim_list (Thm.instantiate inst @{thm conjI}) [thP, thQ] end; fun conj_elim ctxt thPQ = let val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ)) handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]); - val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]); - val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ; - val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ; + val inst = (TVars.empty, Vars.make [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]); + val thP = Thm.implies_elim (Thm.instantiate inst @{thm conjunct1}) thPQ; + val thQ = Thm.implies_elim (Thm.instantiate inst @{thm conjunct2}) thPQ; in (thP, thQ) end; fun conj_elims ctxt th = diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/inductive_set.ML Fri Sep 10 14:59:19 2021 +0200 @@ -221,7 +221,7 @@ fun mk_to_pred_eq ctxt p fs optfs' T thm = let val insts = mk_to_pred_inst ctxt fs; - val thm' = Thm.instantiate ([], insts) thm; + val thm' = Thm.instantiate (TVars.empty, Vars.make insts) thm; val thm'' = (case optfs' of NONE => thm' RS sym @@ -345,7 +345,7 @@ val insts = mk_to_pred_inst ctxt fs in thm |> - Thm.instantiate ([], insts) |> + Thm.instantiate (TVars.empty, Vars.make insts) |> Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs [to_pred_simproc (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: map (Thm.transfer thy) to_pred_simps)]) |> @@ -383,7 +383,7 @@ end) fs; in thm |> - Thm.instantiate ([], insts) |> + Thm.instantiate (TVars.empty, Vars.make insts) |> Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps to_set_simps addsimprocs [strong_ind_simproc pred_arities, \<^simproc>\Collect_mem\]) |> Rule_Cases.save thm diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/lin_arith.ML Fri Sep 10 14:59:19 2021 +0200 @@ -60,8 +60,9 @@ fun is_nat t = (fastype_of1 t = HOLogic.natT); fun mk_nat_thm thy t = - let val ct = Thm.global_cterm_of thy t - in Drule.instantiate_normalize ([], [((("n", 0), HOLogic.natT), ct)]) @{thm le0} end; + let val ct = Thm.global_cterm_of thy t in + Drule.instantiate_normalize (TVars.empty, Vars.make [((("n", 0), HOLogic.natT), ct)]) @{thm le0} + end; end; diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/monomorph.ML --- a/src/HOL/Tools/monomorph.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/monomorph.ML Fri Sep 10 14:59:19 2021 +0200 @@ -165,7 +165,7 @@ let fun cert (ix, (S, T)) = ((ix, S), Thm.ctyp_of ctxt T) fun cert' subst = Vartab.fold (cons o cert) subst [] - in Thm.instantiate (cert' subst, []) end + in Thm.instantiate (TVars.make (cert' subst), Vars.empty) end fun add_new_grounds used_grounds new_grounds thm = let diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/numeral.ML Fri Sep 10 14:59:19 2021 +0200 @@ -64,7 +64,7 @@ val uminus_tvar = tvar \<^sort>\uminus\; val uminus = cterm_of (Const (\<^const_name>\uminus\, TVar uminus_tvar --> TVar uminus_tvar)); -fun instT T v = Thm.instantiate_cterm ([(v, T)], []); +fun instT T v = Thm.instantiate_cterm (TVars.make [(v, T)], Vars.empty); in diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Fri Sep 10 14:59:19 2021 +0200 @@ -594,8 +594,8 @@ fun prove_nz ctxt T t = let - val z = Thm.instantiate_cterm ([(zero_tvar, T)], []) zero - val eq = Thm.instantiate_cterm ([(type_tvar, T)], []) geq + val z = Thm.instantiate_cterm (TVars.make [(zero_tvar, T)], Vars.empty) zero + val eq = Thm.instantiate_cterm (TVars.make [(type_tvar, T)], Vars.empty) geq val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms}) (Thm.apply \<^cterm>\Trueprop\ (Thm.apply \<^cterm>\Not\ diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/record.ML Fri Sep 10 14:59:19 2021 +0200 @@ -1771,7 +1771,8 @@ fun mk_eq_refl ctxt = @{thm equal_refl} |> Thm.instantiate - ([((("'a", 0), \<^sort>\equal\), Thm.ctyp_of ctxt (Logic.varifyT_global extT))], []) + (TVars.make [((("'a", 0), \<^sort>\equal\), Thm.ctyp_of ctxt (Logic.varifyT_global extT))], + Vars.empty) |> Axclass.unoverload ctxt; val ensure_random_record = ensure_sort_record (\<^sort>\random\, mk_random_eq); val ensure_exhaustive_record = diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/reification.ML --- a/src/HOL/Tools/reification.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/reification.ML Fri Sep 10 14:59:19 2021 +0200 @@ -176,7 +176,7 @@ (Vartab.dest tyenv); in ((map (Thm.cterm_of ctxt) fts ~~ replicate (length fts) ctxt, - apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds) + apfst (FWD (Drule.instantiate_normalize (TVars.make ctyenv, Vars.make its) cong))), bds) end handle Pattern.MATCH => decomp_reify da congs (ct, ctxt) bds)) end; @@ -229,10 +229,11 @@ (map (fn n => (n, 0)) xns) tml); val substt = let - val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, [])); + val ih = Drule.cterm_rule (Thm.instantiate (TVars.make subst_ty, Vars.empty)); in map (apply2 ih) (subst_ns @ subst_vs @ cts) end; val th = - (Drule.instantiate_normalize (subst_ty, map (apfst (dest_Var o Thm.term_of)) substt) eq) + (Drule.instantiate_normalize + (TVars.make subst_ty, Vars.make (map (apfst (dest_Var o Thm.term_of)) substt)) eq) RS sym; in (hd (Variable.export ctxt'' ctxt [th]), bds) end) handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds); @@ -270,7 +271,7 @@ val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |> strip_comb; val subst = map_filter (fn Var v => SOME (v, subst (#2 v)) | _ => NONE) vs; - in Thm.instantiate ([], subst) eq end; + in Thm.instantiate (TVars.empty, Vars.make subst) eq end; val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs; val bds = AList.make (K ([], [])) tys; in (ps ~~ Variable.export ctxt' ctxt congs, bds) end @@ -288,7 +289,7 @@ val vs = map (fn Var (v as (_, T)) => (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars; val th' = - Drule.instantiate_normalize ([], map (apsnd (Thm.cterm_of ctxt)) vs) th; + Drule.instantiate_normalize (TVars.empty, Vars.make (map (apsnd (Thm.cterm_of ctxt)) vs)) th; val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th')); in Thm.transitive th'' th' end; diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/sat.ML Fri Sep 10 14:59:19 2021 +0200 @@ -171,7 +171,8 @@ val cLit = snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) in - Thm.instantiate ([], [((("P", 0), HOLogic.boolT), cLit)]) resolution_thm + Thm.instantiate (TVars.empty, Vars.make [((("P", 0), HOLogic.boolT), cLit)]) + resolution_thm end val _ = diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/semiring_normalizer.ML Fri Sep 10 14:59:19 2021 +0200 @@ -81,7 +81,7 @@ let fun h instT = let - val substT = Thm.instantiate (instT, []); + val substT = Thm.instantiate (instT, Vars.empty); val substT_cterm = Drule.cterm_rule substT; val vars' = map substT_cterm vars; @@ -144,8 +144,9 @@ let val (a, b) = Rat.dest x in if b = 1 then Numeral.mk_cnumber cT a else Thm.apply - (Thm.apply (Thm.instantiate_cterm ([(divide_tvar, cT)], []) divide_const) - (Numeral.mk_cnumber cT a)) + (Thm.apply + (Thm.instantiate_cterm (TVars.make [(divide_tvar, cT)], Vars.empty) divide_const) + (Numeral.mk_cnumber cT a)) (Numeral.mk_cnumber cT b) end in @@ -249,7 +250,8 @@ if is_binop ct ct' then Thm.dest_binop ct' else raise CTERM ("dest_binop: bad binop", [ct, ct']) -fun inst_thm inst = Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) inst); +fun inst_thm inst = + Thm.instantiate (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) inst)); val dest_number = Thm.term_of #> HOLogic.dest_number #> snd; val is_number = can dest_number; diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Tools/split_rule.ML Fri Sep 10 14:59:19 2021 +0200 @@ -42,7 +42,7 @@ fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl = let val T' = HOLogic.flatten_tupleT T1 ---> T2; val newt = ap_split T1 T2 (Var (v, T')); - in Thm.instantiate ([], [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end + in Thm.instantiate (TVars.empty, Vars.make [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end | split_rule_var' _ _ rl = rl; @@ -73,7 +73,8 @@ val newt = ap_split' Us U (Var (v, T')); val (vs', insts) = fold mk_tuple ts (vs, []); in - (Drule.instantiate_normalize ([], ((v, T), Thm.cterm_of ctxt newt) :: insts) rl, vs') + (Drule.instantiate_normalize + (TVars.empty, Vars.make (((v, T), Thm.cterm_of ctxt newt) :: insts)) rl, vs') end | complete_split_rule_var _ _ x = x; diff -r 7829d6435c60 -r c2ee8d993d6a src/HOL/Types_To_Sets/unoverload_type.ML --- a/src/HOL/Types_To_Sets/unoverload_type.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML Fri Sep 10 14:59:19 2021 +0200 @@ -40,7 +40,7 @@ val tyenv_list = tyenv |> Vartab.dest |> map (fn (x, (s, TVar (x', _))) => ((x, s), Thm.ctyp_of (Context.proof_of context) (TVar(x', s)))) - val thm'' = Drule.instantiate_normalize (tyenv_list, []) thm' + val thm'' = Drule.instantiate_normalize (TVars.make tyenv_list, Vars.empty) thm' val varify_const = apsnd (subst_TFree "'a" (TVar (tvar, @{sort type}))) #> Const #> Thm.global_cterm_of thy val consts = params_of_sort thy sort diff -r 7829d6435c60 -r c2ee8d993d6a src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Fri Sep 10 14:59:19 2021 +0200 @@ -438,7 +438,7 @@ val T = Thm.typ_of_cterm cv in mth - |> Thm.instantiate ([], [(dest_Var (Thm.term_of cv), number_of T n)]) + |> Thm.instantiate (TVars.empty, Vars.make [(dest_Var (Thm.term_of cv), number_of T n)]) |> rewrite_concl |> discharge_prem handle CTERM _ => mult_by_add n thm diff -r 7829d6435c60 -r c2ee8d993d6a src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Provers/hypsubst.ML Fri Sep 10 14:59:19 2021 +0200 @@ -179,10 +179,10 @@ val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U)); in compose_tac ctxt (true, Drule.instantiate_normalize (instT, - map (apsnd (Thm.cterm_of ctxt)) + Vars.make (map (apsnd (Thm.cterm_of ctxt)) [((ixn, Ts ---> U --> body_type T), u), ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t), - ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl', + ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')])) rl', Thm.nprems_of rl) i end | NONE => no_tac); diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/Isar/class_declaration.ML Fri Sep 10 14:59:19 2021 +0200 @@ -36,12 +36,15 @@ val a_tfree = (Name.aT, base_sort); val a_type = TFree a_tfree; val param_map_const = (map o apsnd) Const param_map; - val param_map_inst = param_map |> map (fn (x, (c, T)) => - let val T' = map_atyps (K a_type) T in ((x, T'), cert (Const (c, T'))) end); + val param_map_inst = + Frees.build (param_map |> fold (fn (x, (c, T)) => + let val T' = map_atyps (K a_type) T + in Frees.add ((x, T'), cert (Const (c, T'))) end)); val const_morph = - Element.instantiate_normalize_morphism ([], param_map_inst); + Element.instantiate_normalize_morphism (TFrees.empty, param_map_inst); val typ_morph = - Element.instantiate_normalize_morphism ([(a_tfree, certT (Term.aT [class]))], []) + Element.instantiate_normalize_morphism + (TFrees.make [(a_tfree, certT (Term.aT [class]))], Frees.empty) val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = thy_ctxt |> Expression.cert_goal_expression ([(class, (("", false), (Expression.Named param_map_const, [])))], []); diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/Isar/code.ML Fri Sep 10 14:59:19 2021 +0200 @@ -799,13 +799,13 @@ val tvs = fold (Term.add_tvars o Thm.prop_of) thms []; val instT = mk_desymbolization (unprefix "'") (prefix "'") (Thm.global_ctyp_of thy o TVar) tvs; - in map (Thm.instantiate (instT, [])) thms end; + in map (Thm.instantiate (TVars.make instT, Vars.empty)) thms end; fun desymbolize_vars thy thm = let val vs = Term.add_vars (Thm.prop_of thm) []; val inst = mk_desymbolization I I (Thm.global_cterm_of thy o Var) vs; - in Thm.instantiate ([], inst) thm end; + in Thm.instantiate (TVars.empty, Vars.make inst) thm end; fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy); @@ -895,14 +895,16 @@ let val mapping = map2 (fn (v, sort) => fn sort' => (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts; - val inst = map2 (fn (v, sort) => fn (_, sort') => - (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping; + val instT = + TVars.build + (fold2 (fn (v, sort) => fn (_, sort') => + TVars.add (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping); val subst = (Term.map_types o map_type_tfree) (fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v))); in thm |> Thm.varifyT_global - |> Thm.instantiate (inst, []) + |> Thm.instantiate (instT, Vars.empty) |> pair subst end; @@ -966,8 +968,9 @@ fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs []; val sorts = map_transpose inter_sorts vss; val vts = Name.invent_names Name.context Name.aT sorts; - val thms' = - map2 (fn vs => Thm.instantiate (vs ~~ map (Thm.ctyp_of ctxt o TFree) vts, [])) vss thms; + fun instantiate vs = + Thm.instantiate (TVars.make (vs ~~ map (Thm.ctyp_of ctxt o TFree) vts), Vars.empty); + val thms' = map2 instantiate vss thms; val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms')))); fun head_conv ct = if can Thm.dest_comb ct then Conv.fun_conv head_conv ct diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/Isar/element.ML Fri Sep 10 14:59:19 2021 +0200 @@ -47,8 +47,7 @@ val transform_witness: morphism -> witness -> witness val conclude_witness: Proof.context -> witness -> thm val pretty_witness: Proof.context -> witness -> Pretty.T - val instantiate_normalize_morphism: - ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism + val instantiate_normalize_morphism: ctyp TFrees.table * cterm Frees.table -> morphism val satisfy_morphism: witness list -> morphism val eq_term_morphism: theory -> term list -> morphism option val eq_morphism: theory -> thm list -> morphism option @@ -208,7 +207,8 @@ SOME C => let val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C); - val th' = Thm.instantiate ([], [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]) th; + val insts = (TVars.empty, Vars.make [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]); + val th' = Thm.instantiate insts th; in (th', true) end | NONE => (th, false)); diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/Isar/expression.ML Fri Sep 10 14:59:19 2021 +0200 @@ -187,14 +187,15 @@ (* instantiation *) val instT = - (type_parms ~~ map Logic.dest_type type_parms'') - |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)); + TFrees.build + (fold2 (fn v => fn T => not (TFree v = T) ? TFrees.add (v, T)) + type_parms (map Logic.dest_type type_parms'')); val cert_inst = - ((map #1 params ~~ - map (Term_Subst.instantiateT_frees (TFrees.make instT)) parm_types) ~~ insts'') - |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)); + Frees.build + (fold2 (fn v => fn t => not (Free v = t) ? Frees.add (v, cert t)) + (map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) insts''); in - (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $> + (Element.instantiate_normalize_morphism (TFrees.map (K certT) instT, cert_inst) $> Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt') end; diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/Isar/generic_target.ML Fri Sep 10 14:59:19 2021 +0200 @@ -328,13 +328,15 @@ val instT = TVars.build (fold2 (fn a => fn b => (case a of TVar v => TVars.add (v, b) | _ => I)) tvars tfrees); - val cinstT = TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) instT []; + val cinstT = TVars.map (K (Thm.ctyp_of ctxt)) instT; val cinst = - map_filter - (fn (Var (xi, T), t) => - SOME ((xi, Term_Subst.instantiateT instT T), - Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t)) - | _ => NONE) (vars ~~ frees); + Vars.build + (fold2 (fn v => fn t => + (case v of + Var (xi, T) => + Vars.add ((xi, Term_Subst.instantiateT instT T), + Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t)) + | _ => I)) vars frees); val result' = Thm.instantiate (cinstT, cinst) result; (*import assumes/defines*) diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/Isar/obtain.ML Fri Sep 10 14:59:19 2021 +0200 @@ -335,7 +335,7 @@ | _ => instT)))); val closed_rule = rule |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) - |> Thm.instantiate (TVars.dest instT, []); + |> Thm.instantiate (instT, Vars.empty); val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt; val vars' = diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/Isar/subgoal.ML --- a/src/Pure/Isar/subgoal.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/Isar/subgoal.ML Fri Sep 10 14:59:19 2021 +0200 @@ -14,7 +14,7 @@ sig type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list, - concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list} + concl: cterm, schematics: ctyp TVars.table * cterm Vars.table} val focus_params: Proof.context -> int -> binding list option -> thm -> focus * thm val focus_params_fixed: Proof.context -> int -> binding list option -> thm -> focus * thm val focus_prems: Proof.context -> int -> binding list option -> thm -> focus * thm @@ -39,7 +39,7 @@ type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list, - concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}; + concl: cterm, schematics: ctyp TVars.table * cterm Vars.table}; fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st = let @@ -56,9 +56,9 @@ val text = asms @ (if do_concl then [concl] else []); val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2; - val schematic_terms = Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst []; + val schematic_terms = Vars.map (K (Thm.cterm_of ctxt3)) inst; - val schematics = (TVars.dest schematic_types, schematic_terms); + val schematics = (schematic_types, schematic_terms); val asms' = map (Thm.instantiate_cterm schematics) asms; val concl' = Thm.instantiate_cterm schematics concl; val (prems, context) = Assumption.add_assumes asms' ctxt3; @@ -100,8 +100,8 @@ in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end; val (inst1, inst2) = split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys)); - - val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th'; + val inst = Vars.build (fold (Vars.add o apfst (Term.dest_Var o Thm.term_of)) inst1); + val th'' = Thm.instantiate (TVars.empty, inst) th'; in ((inst2, th''), ctxt'') end; (* diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/Proof/proof_checker.ML Fri Sep 10 14:59:19 2021 +0200 @@ -81,7 +81,8 @@ val ctye = (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts); in - Thm.instantiate (ctye, []) (Thm.forall_intr_vars (Thm.forall_intr_frees thm')) + Thm.instantiate (TVars.make ctye, Vars.empty) + (Thm.forall_intr_vars (Thm.forall_intr_frees thm')) end; fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) = diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/Tools/rule_insts.ML Fri Sep 10 14:59:19 2021 +0200 @@ -160,8 +160,8 @@ in thm |> Drule.instantiate_normalize - (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars, - map (apsnd (Thm.cterm_of ctxt')) inst_vars) + (TVars.make (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars), + Vars.make (map (apsnd (Thm.cterm_of ctxt')) inst_vars)) |> singleton (Variable.export ctxt' ctxt) |> Rule_Cases.save thm end; @@ -255,10 +255,12 @@ fun lift_var ((a, j), T) = ((a, j + inc), paramTs ---> lift_type T); fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t); - val inst_tvars' = inst_tvars - |> map (fn (((a, i), S), T) => (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T))); - val inst_vars' = inst_vars - |> map (fn (v, t) => (lift_var v, Thm.cterm_of inst_ctxt (lift_term t))); + val inst_tvars' = + TVars.build (inst_tvars |> fold (fn (((a, i), S), T) => + TVars.add (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T)))); + val inst_vars' = + Vars.build (inst_vars |> fold (fn (v, t) => + Vars.add (lift_var v, Thm.cterm_of inst_ctxt (lift_term t)))); val thm' = Thm.lift_rule cgoal thm |> Drule.instantiate_normalize (inst_tvars', inst_vars') @@ -277,8 +279,8 @@ fun var x = ((x, 0), propT); fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT)); val revcut_rl' = - Drule.instantiate_normalize ([], [(var "V", cvar ("V", maxidx + 1)), - (var "W", cvar ("W", maxidx + 1))]) Drule.revcut_rl; + Drule.revcut_rl |> Drule.instantiate_normalize + (TVars.empty, Vars.make [(var "V", cvar ("V", maxidx + 1)), (var "W", cvar ("W", maxidx + 1))]); in (case Seq.list_of (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/conjunction.ML --- a/src/Pure/conjunction.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/conjunction.ML Fri Sep 10 14:59:19 2021 +0200 @@ -102,7 +102,8 @@ fun intr tha thb = Thm.implies_elim (Thm.implies_elim - (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI) + (Thm.instantiate (TVars.empty, Vars.make [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) + conjunctionI) tha) thb; @@ -110,7 +111,7 @@ let val (A, B) = dest_conjunction (Thm.cprop_of th) handle TERM (msg, _) => raise THM (msg, 0, [th]); - val inst = Thm.instantiate ([], [(vA, A), (vB, B)]); + val inst = Thm.instantiate (TVars.empty, Vars.make [(vA, A), (vB, B)]); in (Thm.implies_elim (inst conjunctionD1) th, Thm.implies_elim (inst conjunctionD2) th) diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/drule.ML Fri Sep 10 14:59:19 2021 +0200 @@ -18,8 +18,7 @@ val lift_all: Proof.context -> cterm -> thm -> thm val implies_elim_list: thm -> thm list -> thm val implies_intr_list: cterm list -> thm -> thm - val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> - thm -> thm + val instantiate_normalize: ctyp TVars.table * cterm Vars.table -> thm -> thm val instantiate'_normalize: ctyp option list -> cterm option list -> thm -> thm val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm @@ -192,7 +191,7 @@ | _ => inst))); in th - |> Thm.instantiate ([], Vars.dest inst) + |> Thm.instantiate (TVars.empty, inst) |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps end; @@ -217,15 +216,12 @@ val tvars = TVars.build (fold Thm.add_tvars ths); val the_tvar = the o TVars.lookup tvars; - val instT' = - build (instT |> TVars.fold (fn (v, TVar (b, _)) => - cons (v, Thm.rename_tvar b (the_tvar v)))); + val instT' = instT |> TVars.map (fn v => fn TVar (b, _) => Thm.rename_tvar b (the_tvar v)); - val vars = Vars.build (fold (Thm.add_vars o Thm.instantiate (instT', [])) ths); + val vars = Vars.build (fold (Thm.add_vars o Thm.instantiate (instT', Vars.empty)) ths); val the_var = the o Vars.lookup vars; val inst' = - build (inst |> Vars.fold (fn (v, Var (b, _)) => - cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v))))); + inst |> Vars.map (fn v => fn Var (b, _) => Thm.var (b, Thm.ctyp_of_cterm (the_var v))); in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end; val zero_var_indexes = singleton zero_var_indexes_list; @@ -602,7 +598,9 @@ let val cT = Thm.ctyp_of_cterm ct; val T = Thm.typ_of cT; - in Thm.instantiate ([((("'a", 0), []), cT)], [((("x", 0), T), ct)]) termI end; + in + Thm.instantiate (TVars.make [((("'a", 0), []), cT)], Vars.make [((("x", 0), T), ct)]) termI + end; fun dest_term th = let val cprop = strip_imp_concl (Thm.cprop_of th) in @@ -766,11 +764,12 @@ val (tyenv, _) = fold infer args (Vartab.empty, 0); val instT = - Vartab.fold (fn (xi, (S, T)) => - cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; - val inst = args |> map (fn ((xi, T), cu) => - ((xi, Envir.norm_type tyenv T), - Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); + TVars.build (tyenv |> Vartab.fold (fn (xi, (S, T)) => + TVars.add ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T)))); + val inst = + Vars.build (args |> fold (fn ((xi, T), cu) => + Vars.add ((xi, Envir.norm_type tyenv T), + Thm.instantiate_cterm (instT, Vars.empty) (Thm.transfer_cterm thy cu)))); in instantiate_normalize (instT, inst) th end handle CTERM (msg, _) => raise THM (msg, 0, [raw_th]) | TERM (msg, _) => raise THM (msg, 0, [raw_th]) diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/goal.ML --- a/src/Pure/goal.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/goal.ML Fri Sep 10 14:59:19 2021 +0200 @@ -58,7 +58,7 @@ -------- (init) C \ #C *) -fun init C = Thm.instantiate ([], [((("A", 0), propT), C)]) Drule.protectI; +fun init C = Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), C)]) Drule.protectI; (* A1 \ ... \ An \ C @@ -122,8 +122,8 @@ val tfrees = TFrees.build (fold TFrees.add_tfrees (prop :: As)); val Ts = Names.build (TFrees.fold (Names.add_set o #1 o #1) tfrees); val instT = - build (tfrees |> TFrees.fold (fn ((a, S), _) => - cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S))))); + TVars.build (tfrees |> TFrees.fold (fn ((a, S), _) => + TVars.add (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S))))); val global_prop = Logic.list_implies (As, prop) @@ -142,7 +142,7 @@ val local_result = Thm.future global_result global_prop |> Thm.close_derivation \<^here> - |> Thm.instantiate (instT, []) + |> Thm.instantiate (instT, Vars.empty) |> Drule.forall_elim_list xs |> fold (Thm.elim_implies o Thm.assume) assms |> Thm.solve_constraints; diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/more_thm.ML Fri Sep 10 14:59:19 2021 +0200 @@ -63,7 +63,7 @@ val forall_intr_name: string * cterm -> thm -> thm val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm - val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm + val instantiate_frees: ctyp TFrees.table * cterm Frees.table -> thm -> thm val instantiate': ctyp option list -> cterm option list -> thm -> thm val forall_intr_frees: thm -> thm val forall_intr_vars: thm -> thm @@ -375,26 +375,29 @@ (* instantiate frees *) -fun instantiate_frees ([], []) th = th - | instantiate_frees (instT, inst) th = - let - val idx = Thm.maxidx_of th + 1; - fun index ((a, A), b) = (((a, idx), A), b); - val insts = (map index instT, map index inst); - val tfrees = Names.build (fold (Names.add_set o #1 o #1) instT); - val frees = Names.build (fold (Names.add_set o #1 o #1) inst); +fun instantiate_frees (instT, inst) th = + if TFrees.is_empty instT andalso Frees.is_empty inst then th + else + let + val idx = Thm.maxidx_of th + 1; + fun index ((a, A), b) = (((a, idx), A), b); + val insts = + (TVars.build (TFrees.fold (TVars.add o index) instT), + Vars.build (Frees.fold (Vars.add o index) inst)); + val tfrees = Names.build (TFrees.fold (Names.add_set o #1 o #1) instT); + val frees = Names.build (Frees.fold (Names.add_set o #1 o #1) inst); - val hyps = Thm.chyps_of th; - val inst_cterm = - Thm.generalize_cterm (tfrees, frees) idx #> - Thm.instantiate_cterm insts; - in - th - |> fold_rev Thm.implies_intr hyps - |> Thm.generalize (tfrees, frees) idx - |> Thm.instantiate insts - |> fold (elim_implies o Thm.assume o inst_cterm) hyps - end; + val hyps = Thm.chyps_of th; + val inst_cterm = + Thm.generalize_cterm (tfrees, frees) idx #> + Thm.instantiate_cterm insts; + in + th + |> fold_rev Thm.implies_intr hyps + |> Thm.generalize (tfrees, frees) idx + |> Thm.instantiate insts + |> fold (elim_implies o Thm.assume o inst_cterm) hyps + end; (* instantiate by left-to-right occurrence of variables *) @@ -411,9 +414,9 @@ err "more instantiations than variables in thm"; val instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs; - val thm' = Thm.instantiate (instT, []) thm; + val thm' = Thm.instantiate (TVars.make instT, Vars.empty) thm; val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts; - in Thm.instantiate ([], inst) thm' end; + in Thm.instantiate (TVars.empty, Vars.make inst) thm' end; (* implicit generalization over variables -- canonical order *) @@ -463,7 +466,7 @@ let val T' = Term_Subst.instantiateT instT T in Vars.add (((x, i), T'), cert (Free ((x, T')))) inst end | _ => inst))); - in Thm.instantiate (TVars.dest cinstT, Vars.dest cinst) th end; + in Thm.instantiate (cinstT, cinst) th end; fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; @@ -528,7 +531,7 @@ val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = - Thm.instantiate (recover, []) axm' + Thm.instantiate (TVars.make recover, Vars.empty) axm' |> unvarify_global thy' |> fold elim_implies of_sorts; in ((axm_name, thm), thy') end; @@ -545,7 +548,7 @@ val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = - Thm.instantiate (recover, []) axm' + Thm.instantiate (TVars.make recover, Vars.empty) axm' |> unvarify_global thy' |> fold_rev Thm.implies_intr prems; in ((axm_name, thm), thy') end; diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/morphism.ML --- a/src/Pure/morphism.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/morphism.ML Fri Sep 10 14:59:19 2021 +0200 @@ -43,10 +43,8 @@ val transfer_morphism': Proof.context -> morphism val transfer_morphism'': Context.generic -> morphism val trim_context_morphism: morphism - val instantiate_frees_morphism: - ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism - val instantiate_morphism: - ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism + val instantiate_frees_morphism: ctyp TFrees.table * cterm Frees.table -> morphism + val instantiate_morphism: ctyp TVars.table * cterm Vars.table -> morphism end; structure Morphism: MORPHISM = @@ -134,35 +132,37 @@ (* instantiate *) -fun instantiate_frees_morphism ([], []) = identity - | instantiate_frees_morphism (cinstT, cinst) = - let - val instT = TFrees.build (cinstT |> fold (fn (v, cT) => TFrees.add (v, Thm.typ_of cT))); - val inst = Frees.build (cinst |> fold (fn (v, ct) => Frees.add (v, Thm.term_of ct))); - in - morphism "instantiate_frees" - {binding = [], - typ = - if TFrees.is_empty instT then [] - else [Term_Subst.instantiateT_frees instT], - term = [Term_Subst.instantiate_frees (instT, inst)], - fact = [map (Thm.instantiate_frees (cinstT, cinst))]} - end; +fun instantiate_frees_morphism (cinstT, cinst) = + if TFrees.is_empty cinstT andalso Frees.is_empty cinst then identity + else + let + val instT = TFrees.map (K Thm.typ_of) cinstT; + val inst = Frees.map (K Thm.term_of) cinst; + in + morphism "instantiate_frees" + {binding = [], + typ = + if TFrees.is_empty instT then [] + else [Term_Subst.instantiateT_frees instT], + term = [Term_Subst.instantiate_frees (instT, inst)], + fact = [map (Thm.instantiate_frees (cinstT, cinst))]} + end; -fun instantiate_morphism ([], []) = identity - | instantiate_morphism (cinstT, cinst) = - let - val instT = TVars.build (cinstT |> fold (fn (v, cT) => TVars.add (v, Thm.typ_of cT))); - val inst = Vars.build (cinst |> fold (fn (v, ct) => Vars.add (v, Thm.term_of ct))); - in - morphism "instantiate" - {binding = [], - typ = - if TVars.is_empty instT then [] - else [Term_Subst.instantiateT instT], - term = [Term_Subst.instantiate (instT, inst)], - fact = [map (Thm.instantiate (cinstT, cinst))]} - end; +fun instantiate_morphism (cinstT, cinst) = + if TVars.is_empty cinstT andalso Vars.is_empty cinst then identity + else + let + val instT = TVars.map (K Thm.typ_of) cinstT; + val inst = Vars.map (K Thm.term_of) cinst; + in + morphism "instantiate" + {binding = [], + typ = + if TVars.is_empty instT then [] + else [Term_Subst.instantiateT instT], + term = [Term_Subst.instantiate (instT, inst)], + fact = [map (Thm.instantiate (cinstT, cinst))]} + end; end; diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/raw_simplifier.ML Fri Sep 10 14:59:19 2021 +0200 @@ -1226,7 +1226,8 @@ val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq); val eq' = Thm.implies_elim - (Thm.instantiate ([], [(vA, prem), (vB, lhs), (vC, rhs)]) Drule.imp_cong) + (Thm.instantiate (TVars.empty, Vars.make [(vA, prem), (vB, lhs), (vC, rhs)]) + Drule.imp_cong) (Thm.implies_intr prem eq); in if not r then eq' @@ -1237,9 +1238,11 @@ in Thm.transitive (Thm.transitive - (Thm.instantiate ([], [(vA, prem'), (vB, prem), (vC, concl)]) Drule.swap_prems_eq) + (Thm.instantiate (TVars.empty, Vars.make [(vA, prem'), (vB, prem), (vC, concl)]) + Drule.swap_prems_eq) eq') - (Thm.instantiate ([], [(vA, prem), (vB, prem''), (vC, concl)]) Drule.swap_prems_eq) + (Thm.instantiate (TVars.empty, Vars.make [(vA, prem), (vB, prem''), (vC, concl)]) + Drule.swap_prems_eq) end end diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/tactic.ML --- a/src/Pure/tactic.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/tactic.ML Fri Sep 10 14:59:19 2021 +0200 @@ -164,14 +164,15 @@ val template = Drule.list_implies (As, C); val inst = - (dest_Free (Thm.term_of C), Thm.cconcl_of st) :: - Ctermtab.fold (fn (ct, i) => cons ((Name.bound i, propT), ct)) tab []; + Frees.build + (Frees.add (dest_Free (Thm.term_of C), Thm.cconcl_of st) #> + Ctermtab.fold (fn (ct, i) => Frees.add ((Name.bound i, propT), ct)) tab); in Thm.assume template |> fold (Thm.elim_implies o Thm.assume) As |> fold_rev Thm.implies_intr As' |> Thm.implies_intr template - |> Thm.instantiate_frees ([], inst) + |> Thm.instantiate_frees (TFrees.empty, inst) |> Thm.elim_implies st end; in Seq.single st' end; diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/thm.ML Fri Sep 10 14:59:19 2021 +0200 @@ -56,10 +56,8 @@ val lambda: cterm -> cterm -> cterm val adjust_maxidx_cterm: int -> cterm -> cterm val incr_indexes_cterm: int -> cterm -> cterm - val match: cterm * cterm -> - ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list - val first_order_match: cterm * cterm -> - ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list + val match: cterm * cterm -> ctyp TVars.table * cterm Vars.table + val first_order_match: cterm * cterm -> ctyp TVars.table * cterm Vars.table (*theorems*) val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a val fold_atomic_ctyps: {hyps: bool} -> (typ -> bool) -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a @@ -157,10 +155,8 @@ val generalize: Names.set * Names.set -> int -> thm -> thm val generalize_cterm: Names.set * Names.set -> int -> cterm -> cterm val generalize_ctyp: Names.set -> int -> ctyp -> ctyp - val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> - thm -> thm - val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> - cterm -> cterm + val instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm + val instantiate_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm val trivial: cterm -> thm val of_class: ctyp * class -> thm val unconstrainT: thm -> thm @@ -651,7 +647,10 @@ let val T = Envir.subst_type Tinsts U in (((x, i), T), Cterm {t = t, T = T, cert = cert, maxidx = maxidx2, sorts = sorts}) end; - in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; + in + (TVars.build (Vartab.fold (TVars.add o mk_cTinst) Tinsts), + Vars.build (Vartab.fold (Vars.add o mk_ctinst) tinsts)) + end; in @@ -1630,12 +1629,12 @@ val add_instT_sorts = add_sorts (fn Ctyp {sorts, ...} => sorts); val add_inst_sorts = add_sorts (fn Cterm {sorts, ...} => sorts); -fun add_instT thy (v as (_, S), Ctyp {T = U, maxidx, ...}) = - if Sign.of_sort thy (U, S) then TVars.add (v, (U, maxidx)) +fun make_instT thy (v as (_, S)) (Ctyp {T = U, maxidx, ...}) = + if Sign.of_sort thy (U, S) then (U, maxidx) else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy S, [U], []); -fun add_inst thy (v as (_, T), Cterm {t = u, T = U, maxidx, ...}) = - if T = U then Vars.add (v, (u, maxidx)) +fun make_inst thy (v as (_, T)) (Cterm {t = u, T = U, maxidx, ...}) = + if T = U then (u, maxidx) else let fun pretty_typing t ty = @@ -1651,17 +1650,18 @@ fun prep_insts (instT, inst) (cert, sorts) = let val cert' = cert - |> fold add_instT_cert instT - |> fold add_inst_cert inst; - val thy' = Context.certificate_theory cert' - handle ERROR msg => raise CONTEXT (msg, map #2 instT, map #2 inst, [], NONE); + |> TVars.fold add_instT_cert instT + |> Vars.fold add_inst_cert inst; + val thy' = + Context.certificate_theory cert' handle ERROR msg => + raise CONTEXT (msg, TVars.dest instT |> map #2, Vars.dest inst |> map #2, [], NONE); val sorts' = sorts - |> fold add_instT_sorts instT - |> fold add_inst_sorts inst; + |> TVars.fold add_instT_sorts instT + |> Vars.fold add_inst_sorts inst; - val instT' = TVars.build (fold (add_instT thy') instT); - val inst' = Vars.build (fold (add_inst thy') inst); + val instT' = TVars.map (make_instT thy') instT; + val inst' = Vars.map (make_inst thy') inst; in ((instT', inst'), (cert', sorts')) end; in @@ -1669,49 +1669,51 @@ (*Left-to-right replacements: ctpairs = [..., (vi, ti), ...]. Instantiates distinct Vars by terms of same type. Does NOT normalize the resulting theorem!*) -fun instantiate ([], []) th = th - | instantiate (instT, inst) th = - let - val Thm (der, {cert, hyps, constraints, shyps, tpairs, prop, ...}) = th; - val ((instT', inst'), (cert', shyps')) = prep_insts (instT, inst) (cert, shyps) - handle CONTEXT (msg, cTs, cts, ths, context) => - raise CONTEXT (msg, cTs, cts, th :: ths, context); +fun instantiate (instT, inst) th = + if TVars.is_empty instT andalso Vars.is_empty inst then th + else + let + val Thm (der, {cert, hyps, constraints, shyps, tpairs, prop, ...}) = th; + val ((instT', inst'), (cert', shyps')) = prep_insts (instT, inst) (cert, shyps) + handle CONTEXT (msg, cTs, cts, ths, context) => + raise CONTEXT (msg, cTs, cts, th :: ths, context); - val subst = Term_Subst.instantiate_maxidx (instT', inst'); - val (prop', maxidx1) = subst prop ~1; - val (tpairs', maxidx') = - fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1; + val subst = Term_Subst.instantiate_maxidx (instT', inst'); + val (prop', maxidx1) = subst prop ~1; + val (tpairs', maxidx') = + fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1; - val thy' = Context.certificate_theory cert'; - val constraints' = - TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) - instT' constraints; - in - Thm (deriv_rule1 - (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d) der, - {cert = cert', - tags = [], - maxidx = maxidx', - constraints = constraints', - shyps = shyps', - hyps = hyps, - tpairs = tpairs', - prop = prop'}) - |> solve_constraints - end - handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); + val thy' = Context.certificate_theory cert'; + val constraints' = + TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) + instT' constraints; + in + Thm (deriv_rule1 + (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d) der, + {cert = cert', + tags = [], + maxidx = maxidx', + constraints = constraints', + shyps = shyps', + hyps = hyps, + tpairs = tpairs', + prop = prop'}) + |> solve_constraints + end + handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); -fun instantiate_cterm ([], []) ct = ct - | instantiate_cterm (instT, inst) ct = - let - val Cterm {cert, t, T, sorts, ...} = ct; - val ((instT', inst'), (cert', sorts')) = prep_insts (instT, inst) (cert, sorts); - val subst = Term_Subst.instantiate_maxidx (instT', inst'); - val substT = Term_Subst.instantiateT_maxidx instT'; - val (t', maxidx1) = subst t ~1; - val (T', maxidx') = substT T maxidx1; - in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end - handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); +fun instantiate_cterm (instT, inst) ct = + if TVars.is_empty instT andalso Vars.is_empty inst then ct + else + let + val Cterm {cert, t, T, sorts, ...} = ct; + val ((instT', inst'), (cert', sorts')) = prep_insts (instT, inst) (cert, sorts); + val subst = Term_Subst.instantiate_maxidx (instT', inst'); + val substT = Term_Subst.instantiateT_maxidx instT'; + val (t', maxidx1) = subst t ~1; + val (T', maxidx') = substT T maxidx1; + in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end + handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); end; @@ -2278,7 +2280,7 @@ val names = Name.invent Name.context Name.aT (length tvars); val tinst = map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names; - in instantiate (tinst, []) thm end + in instantiate (TVars.make tinst, Vars.empty) thm end (* class relations *) diff -r 7829d6435c60 -r c2ee8d993d6a src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/variable.ML Fri Sep 10 14:59:19 2021 +0200 @@ -618,7 +618,7 @@ let val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT; - val ths' = map (Thm.instantiate (TVars.dest instT', [])) ths; + val ths' = map (Thm.instantiate (instT', Vars.empty)) ths; in ((instT', ths'), ctxt') end; fun import_prf is_open prf ctxt = @@ -632,7 +632,7 @@ val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT; val inst' = Vars.map (K (Thm.cterm_of ctxt')) inst; - val ths' = map (Thm.instantiate (TVars.dest instT', Vars.dest inst')) ths; + val ths' = map (Thm.instantiate (instT', inst')) ths; in (((instT', inst'), ths'), ctxt') end; fun import_vars ctxt th = diff -r 7829d6435c60 -r c2ee8d993d6a src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Tools/Code/code_preproc.ML Fri Sep 10 14:59:19 2021 +0200 @@ -213,7 +213,7 @@ if eq_list (eq_fst (op =)) (vs_normalized, vs_original) then (K I, ct) else - (K (Thm.instantiate (normalization, []) o Thm.varifyT_global), + (K (Thm.instantiate (TVars.make normalization, Vars.empty) o Thm.varifyT_global), Thm.cterm_of ctxt (map_types normalize t)) end; diff -r 7829d6435c60 -r c2ee8d993d6a src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Fri Sep 10 14:59:19 2021 +0200 @@ -174,11 +174,11 @@ val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); (* certified instantiations for types *) - val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts; + val ctyp_insts = TVars.make (map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts); (* type instantiated versions *) - val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; - val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule; + val tgt_th_tyinst = Thm.instantiate (ctyp_insts,Vars.empty) target_thm; + val rule_tyinst = Thm.instantiate (ctyp_insts,Vars.empty) rule; val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts; (* type instanitated outer term *) @@ -198,10 +198,10 @@ (* create certms of instantiations *) val cinsts_tyinst = - map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst; + Vars.make (map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst); (* The instantiated rule *) - val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst); + val rule_inst = rule_tyinst |> Thm.instantiate (TVars.empty, cinsts_tyinst); (* Create a table of vars to be renamed after instantiation - ie other uninstantiated vars in the hyps the *instantiated* rule @@ -217,7 +217,7 @@ val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst); val (cprems, abstract_rule_inst) = rule_inst - |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings) + |> Thm.instantiate (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) cterm_renamings)) |> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst; val specific_tgt_rule = Conv.fconv_rule Drule.beta_eta_conversion @@ -226,8 +226,8 @@ (* create an instantiated version of the target thm *) val tgt_th_inst = tgt_th_tyinst - |> Thm.instantiate ([], cinsts_tyinst) - |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings); + |> Thm.instantiate (TVars.empty, cinsts_tyinst) + |> Thm.instantiate (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) cterm_renamings)); val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings; in diff -r 7829d6435c60 -r c2ee8d993d6a src/Tools/coherent.ML --- a/src/Tools/coherent.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Tools/coherent.ML Fri Sep 10 14:59:19 2021 +0200 @@ -175,13 +175,14 @@ val _ = cond_trace ctxt (fn () => Pretty.string_of (Pretty.big_list "asms:" (map (Thm.pretty_thm ctxt) asms))); + val instT = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye); + val inst = + map (fn (ixn, (T, t)) => + ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @ + map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts; val th' = Drule.implies_elim_list - (Thm.instantiate - (map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye), - map (fn (ixn, (T, t)) => - ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @ - map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts) th) + (Thm.instantiate (TVars.make instT, Vars.make inst) th) (map (nth asms) is); val (_, cases) = dest_elim (Thm.prop_of th'); in diff -r 7829d6435c60 -r c2ee8d993d6a src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Tools/induct.ML Fri Sep 10 14:59:19 2021 +0200 @@ -593,13 +593,16 @@ local -fun dest_env ctxt env = +fun insts_env ctxt env = let val pairs = Vartab.dest (Envir.term_env env); val types = Vartab.dest (Envir.type_env env); val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs; val xs = map #1 pairs ~~ map Thm.typ_of_cterm ts; - in (map (fn (ai, (S, T)) => ((ai, S), Thm.ctyp_of ctxt T)) types, xs ~~ ts) end; + val instT = + TVars.build (types |> fold (fn (ai, (S, T)) => TVars.add ((ai, S), Thm.ctyp_of ctxt T))); + val inst = Vars.build (fold2 (fn x => fn t => Vars.add (x, t)) xs ts); + in (instT, inst) end; in @@ -620,7 +623,7 @@ in Unify.smash_unifiers (Context.Proof ctxt) [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule')) - |> Seq.map (fn env => Drule.instantiate_normalize (dest_env ctxt env) rule') + |> Seq.map (fn env => Drule.instantiate_normalize (insts_env ctxt env) rule') end end handle General.Subscript => Seq.empty; diff -r 7829d6435c60 -r c2ee8d993d6a src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Tools/misc_legacy.ML Fri Sep 10 14:59:19 2021 +0200 @@ -185,7 +185,8 @@ fold Term.add_vars (Logic.strip_imp_prems prop) [] and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [] val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars - val st' = Thm.instantiate ([], map mk_inst subgoal_insts) st + val st' = + Thm.instantiate (TVars.empty, Vars.build (fold (Vars.add o mk_inst) subgoal_insts)) st val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st') val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs) in (*restore the unknowns to the hypotheses*) @@ -247,7 +248,9 @@ fun thaw i th' = (*i is non-negative increment for Var indexes*) th' |> forall_intr_list (map #2 insts) |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts) - in (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw) end + in + (Thm.instantiate (TVars.empty, Vars.build (fold (Vars.add o apfst (dest_Var o Thm.term_of)) insts)) fth, thaw) + end end; end; diff -r 7829d6435c60 -r c2ee8d993d6a src/Tools/nbe.ML --- a/src/Tools/nbe.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Tools/nbe.ML Fri Sep 10 14:59:19 2021 +0200 @@ -109,7 +109,7 @@ val tvars = Term.add_tvars (#1 (Logic.dest_equals (Logic.strip_imp_concl (Thm.prop_of thm)))) []; val instT = map2 (fn v => fn (_, (_, (cT, _))) => (v, cT)) tvars vs_tab; - in Thm.instantiate (instT, []) thm end; + in Thm.instantiate (TVars.make instT, Vars.empty) thm end; fun of_class (TFree (v, _), class) = the (AList.lookup (op =) ((snd o snd o the o AList.lookup (op =) vs_tab) v) class) | of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ ctxt T); diff -r 7829d6435c60 -r c2ee8d993d6a src/ZF/Tools/cartprod.ML --- a/src/ZF/Tools/cartprod.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/ZF/Tools/cartprod.ML Fri Sep 10 14:59:19 2021 +0200 @@ -108,8 +108,8 @@ val newt = ap_split T1 T2 (Var(v,T')) in remove_split ctxt - (Drule.instantiate_normalize ([], - [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl) + (Drule.instantiate_normalize (TVars.empty, + Vars.make [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl) end | split_rule_var _ (t,T,rl) = rl; diff -r 7829d6435c60 -r c2ee8d993d6a src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/ZF/Tools/inductive_package.ML Fri Sep 10 14:59:19 2021 +0200 @@ -508,7 +508,7 @@ The name "x.1" comes from the "RS spec" !*) val inst = case elem_frees of [_] => I - | _ => Drule.instantiate_normalize ([], [(((("x",1), Ind_Syntax.iT)), + | _ => Drule.instantiate_normalize (TVars.empty, Vars.make [(((("x",1), Ind_Syntax.iT)), Thm.global_cterm_of thy4 elem_tuple)]); (*strip quantifier and the implication*)