--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue Apr 18 22:24:48 2023 +0200
@@ -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 (TVars.empty, Vars.make [(U_v,cU)])) nmi
+ nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make1 (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 (TVars.empty, Vars.make [(U_v,cU)])) npi
+ npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make1 (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 (TVars.empty, Vars.make [(U_v,cU)])) ld
+ ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make1 (U_v,cU))) ld
fun decomp_mpinf fm =
case Thm.term_of fm of
--- a/src/HOL/Library/cconv.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Library/cconv.ML Tue Apr 18 22:24:48 2023 +0200
@@ -132,7 +132,7 @@
end
val rule = abstract_rule_thm x
val inst = Thm.match (hd (Drule.cprems_of rule), mk_concl eq)
- val gen = (Names.empty, Names.make_set [#1 (dest_Free v)])
+ val gen = (Names.empty, Names.make1_set (#1 (dest_Free v)))
in
(Drule.instantiate_normalize inst rule OF [Drule.generalize gen eq])
|> Drule.zero_var_indexes
--- a/src/HOL/Library/old_recdef.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Library/old_recdef.ML Tue Apr 18 22:24:48 2023 +0200
@@ -308,7 +308,7 @@
Conv.fconv_rule Drule.beta_eta_conversion
(case_thm
|> Thm.instantiate (TVars.make type_cinsts, Vars.empty)
- |> Thm.instantiate (TVars.empty, Vars.make [(Pv, abs_ct), (Dv, free_ct)]))
+ |> Thm.instantiate (TVars.empty, Vars.make2 (Pv, abs_ct) (Dv, free_ct)))
end;
@@ -1124,7 +1124,7 @@
in
fun SPEC tm thm =
let val gspec' =
- Drule.instantiate_normalize (TVars.make [(TV, Thm.ctyp_of_cterm tm)], Vars.empty) gspec
+ Drule.instantiate_normalize (TVars.make1 (TV, Thm.ctyp_of_cterm tm), Vars.empty) gspec
in thm RS (Thm.forall_elim tm gspec') end
end;
--- a/src/HOL/Nominal/nominal_datatype.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue Apr 18 22:24:48 2023 +0200
@@ -1571,8 +1571,8 @@
(Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
(fn {context = ctxt, ...} =>
dresolve_tac ctxt [Thm.instantiate (TVars.empty,
- Vars.make [((("pi", 0), permT),
- Thm.global_cterm_of thy11 (Const (\<^const_name>\<open>rev\<close>, permT --> permT) $ pi))]) th] 1 THEN
+ Vars.make1 ((("pi", 0), permT),
+ Thm.global_cterm_of thy11 (Const (\<^const_name>\<open>rev\<close>, 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,9 +1662,9 @@
SUBPROOF (fn {context = ctxt', prems = prems', params = [(_, a), (_, b)], ...} =>
EVERY [cut_facts_tac [rec_prem] 1,
resolve_tac ctxt' [Thm.instantiate (TVars.empty,
- Vars.make [((("pi", 0), mk_permT aT),
+ Vars.make1 ((("pi", 0), mk_permT aT),
Thm.cterm_of ctxt'
- (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th] 1,
+ (perm_of_pair (Thm.term_of a, Thm.term_of b)))) eqvt_th] 1,
asm_simp_tac (put_simpset HOL_ss ctxt' addsimps
(prems' @ perm_swap @ perm_fresh_fresh)) 1]) ctxt 1,
resolve_tac ctxt [rec_prem] 1,
@@ -1882,7 +1882,7 @@
val l = find_index (equal T) dt_atomTs;
val th = nth (nth rec_equiv_thms' l) k;
val th' = Thm.instantiate (TVars.empty,
- Vars.make [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th;
+ Vars.make1 ((("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))
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Tue Apr 18 22:24:48 2023 +0200
@@ -153,7 +153,7 @@
[Var v] =>
Seq.single
(Thm.instantiate (TVars.empty,
- Vars.make [(v, Thm.cterm_of ctxt (fold_rev Term.abs params (Bound 0)))]) st)
+ Vars.make1 (v, Thm.cterm_of ctxt (fold_rev Term.abs params (Bound 0)))) st)
| _ => error "fresh_fun_simp: Too many variables, please report."
end
in
--- a/src/HOL/Real_Asymp/multiseries_expansion.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Real_Asymp/multiseries_expansion.ML Tue Apr 18 22:24:48 2023 +0200
@@ -218,7 +218,7 @@
case tvs of
[v] =>
let
- val thm' = Thm.instantiate (TVars.make [(v, Thm.ctyp_of_cterm ct)], Vars.empty) thm
+ val thm' = Thm.instantiate (TVars.make1 (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 (TVars.empty, Vars.make (vs ~~ cts)) thm'
--- a/src/HOL/Statespace/distinct_tree_prover.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Tue Apr 18 22:24:48 2023 +0200
@@ -310,8 +310,8 @@
val [alphaI] = #2 (dest_Type T);
in
Thm.instantiate
- (TVars.make [(alpha, Thm.ctyp_of ctxt alphaI)],
- Vars.make [((v, treeT alphaI), ct')]) @{thm subtract_Tip}
+ (TVars.make1 (alpha, Thm.ctyp_of ctxt alphaI),
+ Vars.make1 ((v, treeT alphaI), ct')) @{thm subtract_Tip}
end
| subtractProver ctxt (Const (\<^const_name>\<open>Node\<close>, nT) $ l $ x $ d $ r) ct dist_thm =
let
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Tue Apr 18 22:24:48 2023 +0200
@@ -943,7 +943,7 @@
end
fun instantiate_tac from to =
- PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(from, to)]))
+ PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make1 (from, to)))
val tactic =
if is_none var_opt then no_tac
--- a/src/HOL/Tools/Argo/argo_real.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Argo/argo_real.ML Tue Apr 18 22:24:48 2023 +0200
@@ -208,7 +208,7 @@
fun add_cmp_conv ctxt n thm =
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)
+ (Thm.instantiate (TVars.empty, Vars.make1 (v, Thm.cterm_of ctxt (mk_number n))) thm)
end
fun mul_cmp_conv ctxt n pos_thm neg_thm =
--- a/src/HOL/Tools/Argo/argo_tactic.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Tue Apr 18 22:24:48 2023 +0200
@@ -656,7 +656,7 @@
(* normalizing goals *)
-fun instantiate v ct = Thm.instantiate (TVars.empty, Vars.make [(v, ct)])
+fun instantiate v ct = Thm.instantiate (TVars.empty, Vars.make1 (v, ct))
fun instantiate_elim_rule thm =
let
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Apr 18 22:24:48 2023 +0200
@@ -851,7 +851,7 @@
|> unfold_thms lthy [dtor_ctor];
in
(fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans))
- |> Drule.generalize (Names.empty, Names.make_set [y_s])
+ |> Drule.generalize (Names.empty, Names.make1_set y_s)
end;
val map_thms =
@@ -930,7 +930,7 @@
|> infer_instantiate' lthy (replicate live NONE @
[SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
|> unfold_thms lthy [dtor_ctor]
- |> Drule.generalize (Names.empty, Names.make_set [y_s, z_s])
+ |> Drule.generalize (Names.empty, Names.make2_set y_s z_s)
end;
val rel_inject_thms =
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Apr 18 22:24:48 2023 +0200
@@ -160,7 +160,7 @@
val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
in
Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split
- |> Drule.generalize (Names.empty, Names.make_set [s])
+ |> Drule.generalize (Names.empty, Names.make1_set s)
end
| _ => split);
--- a/src/HOL/Tools/Function/induction_schema.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Tue Apr 18 22:24:48 2023 +0200
@@ -381,7 +381,7 @@
val res = Conjunction.intr_balanced (map_index project branches)
|> fold_rev Thm.implies_intr (map Thm.cprop_of newgoals @ steps)
- |> Drule.generalize (Names.empty, Names.make_set [Rn])
+ |> Drule.generalize (Names.empty, Names.make1_set Rn)
val nbranches = length branches
val npres = length pres
--- a/src/HOL/Tools/Function/partial_function.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Apr 18 22:24:48 2023 +0200
@@ -209,7 +209,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 (TVars.empty, Vars.make [(P_var, P_inst), (x_var, x_inst)])
+ |> Thm.instantiate (TVars.empty, Vars.make2 (P_var, P_inst) (x_var, x_inst))
|> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
|> singleton (Variable.export ctxt' ctxt)
in
--- a/src/HOL/Tools/Function/relation.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Function/relation.ML Tue Apr 18 22:24:48 2023 +0200
@@ -19,7 +19,7 @@
SUBGOAL (fn (goal, _) =>
(case Term.add_vars goal [] of
[v as (_, T)] =>
- PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(v, Thm.cterm_of ctxt (inst T))]))
+ PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make1 (v, Thm.cterm_of ctxt (inst T))))
| _ => no_tac));
fun relation_tac ctxt rel i =
@@ -39,7 +39,7 @@
|> map_types Type_Infer.paramify_vars
|> Type.constraint T
|> Syntax.check_term ctxt;
- in PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(v, Thm.cterm_of ctxt rel')])) end
+ in PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make1 (v, Thm.cterm_of ctxt rel'))) end
| _ => no_tac));
fun relation_infer_tac ctxt rel i =
--- a/src/HOL/Tools/Meson/meson.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Tue Apr 18 22:24:48 2023 +0200
@@ -358,7 +358,7 @@
Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
val spec' = spec
|> Thm.instantiate
- (TVars.empty, Vars.make [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]);
+ (TVars.empty, Vars.make1 (spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var))));
in (th RS spec', ctxt') end
end;
--- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Apr 18 22:24:48 2023 +0200
@@ -42,9 +42,9 @@
fun transform_elim_theorem th =
(case Thm.concl_of th of (*conclusion variable*)
\<^Const_>\<open>Trueprop for \<open>Var (v as (_, \<^Type>\<open>bool\<close>))\<close>\<close> =>
- Thm.instantiate (TVars.empty, Vars.make [(v, cfalse)]) th
+ Thm.instantiate (TVars.empty, Vars.make1 (v, cfalse)) th
| Var (v as (_, \<^Type>\<open>prop\<close>)) =>
- Thm.instantiate (TVars.empty, Vars.make [(v, ctp_false)]) th
+ Thm.instantiate (TVars.empty, Vars.make1 (v, ctp_false)) th
| _ => th)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Apr 18 22:24:48 2023 +0200
@@ -943,7 +943,7 @@
Thm.instantiate
(TVars.make [(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
(dest_TVar uninst_T', Thm.ctyp_of ctxt' T')],
- Vars.make [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
+ Vars.make1 ((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'
--- a/src/HOL/Tools/Qelim/cooper.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Apr 18 22:24:48 2023 +0200
@@ -507,17 +507,17 @@
then
(bl,b0,decomp_minf,
fn B => (map (fn th =>
- Thm.implies_elim (Thm.instantiate (TVars.empty, Vars.make [(B_v,B), (D_v,cd)]) th) dp)
+ Thm.implies_elim (Thm.instantiate (TVars.empty, Vars.make2 (B_v,B) (D_v,cd)) th) dp)
[bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
- (map (Thm.instantiate (TVars.empty, Vars.make [(B_v,B), (D_v,cd)]))
+ (map (Thm.instantiate (TVars.empty, Vars.make2 (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 (TVars.empty, Vars.make [(A_v,A), (D_v,cd)]) th) dp)
+ Thm.implies_elim (Thm.instantiate (TVars.empty, Vars.make2 (A_v,A) (D_v,cd)) th) dp)
[aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
- (map (Thm.instantiate (TVars.empty, Vars.make [(A_v,A), (D_v,cd)]))
+ (map (Thm.instantiate (TVars.empty, Vars.make2 (A_v,A) (D_v,cd)))
[asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
asetdisj,infDconj, infDdisj]),cppi)
val cpth =
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Tue Apr 18 22:24:48 2023 +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 (TVars.make [(a_v, icT)], Vars.empty);
+ val inst = Thm.instantiate_cterm (TVars.make1 (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>\<open>0::natural\<close> eq,
@@ -105,9 +105,9 @@
val cT_rhs = inst pt_rhs |> Thm.term_of |> dest_Var;
val rule = @{thm random_aux_rec}
|> Drule.instantiate_normalize
- (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)]);
+ (TVars.make1 (a_v, icT),
+ Vars.make2 (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])
THEN ALLGOALS (simp_tac (put_simpset rew_ss ctxt))
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Apr 18 22:24:48 2023 +0200
@@ -477,7 +477,7 @@
else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
val thm4 =
Drule.instantiate_normalize
- (TVars.empty, Vars.make [(dest_Var insp, Thm.cterm_of ctxt inst)]) thm3
+ (TVars.empty, Vars.make1 (dest_Var insp, Thm.cterm_of ctxt inst)) thm3
in
Conv.rewr_conv thm4 ctrm
end
--- a/src/HOL/Tools/SMT/smt_normalize.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Apr 18 22:24:48 2023 +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 (TVars.empty, Vars.make [(dest_Var (Thm.term_of cv), ct)]) thm end
+ in Thm.instantiate (TVars.empty, Vars.make1 (dest_Var (Thm.term_of cv), ct)) thm end
in
fun instantiate_elim thm =
@@ -401,7 +401,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 (TVars.empty, Vars.make [(var, ct)]) int_thm) cts)
+ else (thms, map (fn ct => Thm.instantiate (TVars.empty, Vars.make1 (var, ct)) int_thm) cts)
end
val setup_nat_as_int =
--- a/src/HOL/Tools/numeral.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/numeral.ML Tue Apr 18 22:24:48 2023 +0200
@@ -64,7 +64,7 @@
val uminus_tvar = tvar \<^sort>\<open>uminus\<close>;
val uminus = cterm_of (Const (\<^const_name>\<open>uminus\<close>, TVar uminus_tvar --> TVar uminus_tvar));
-fun instT T v = Thm.instantiate_cterm (TVars.make [(v, T)], Vars.empty);
+fun instT T v = Thm.instantiate_cterm (TVars.make1 (v, T), Vars.empty);
in
--- a/src/HOL/Tools/numeral_simprocs.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Tue Apr 18 22:24:48 2023 +0200
@@ -591,8 +591,8 @@
fun prove_nz ctxt T t =
let
- 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 z = Thm.instantiate_cterm (TVars.make1 (zero_tvar, T), Vars.empty) zero
+ val eq = Thm.instantiate_cterm (TVars.make1 (type_tvar, T), Vars.empty) geq
val th =
Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
(Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close>
--- a/src/HOL/Tools/semiring_normalizer.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Tue Apr 18 22:24:48 2023 +0200
@@ -144,7 +144,7 @@
in if b = 1 then Numeral.mk_cnumber cT a
else Thm.apply
(Thm.apply
- (Thm.instantiate_cterm (TVars.make [(divide_tvar, cT)], Vars.empty) divide_const)
+ (Thm.instantiate_cterm (TVars.make1 (divide_tvar, cT), Vars.empty) divide_const)
(Numeral.mk_cnumber cT a))
(Numeral.mk_cnumber cT b)
end
--- a/src/HOL/Tools/split_rule.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/HOL/Tools/split_rule.ML Tue Apr 18 22:24:48 2023 +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 (TVars.empty, Vars.make [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end
+ in Thm.instantiate (TVars.empty, Vars.make1 (dest_Var t, Thm.cterm_of ctxt newt)) rl end
| split_rule_var' _ _ rl = rl;
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Apr 18 22:24:48 2023 +0200
@@ -437,7 +437,7 @@
val T = Thm.typ_of_cterm cv
in
mth
- |> Thm.instantiate (TVars.empty, Vars.make [(dest_Var (Thm.term_of cv), number_of T n)])
+ |> Thm.instantiate (TVars.empty, Vars.make1 (dest_Var (Thm.term_of cv), number_of T n))
|> rewrite_concl
|> discharge_prem
handle CTERM _ => mult_by_add n thm
--- a/src/Pure/Isar/class_declaration.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/Isar/class_declaration.ML Tue Apr 18 22:24:48 2023 +0200
@@ -44,7 +44,7 @@
Element.instantiate_normalize_morphism (TFrees.empty, param_map_inst);
val typ_morph =
Element.instantiate_normalize_morphism
- (TFrees.make [(a_tfree, certT (Term.aT [class]))], Frees.empty)
+ (TFrees.make1 (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, [])))], []);
--- a/src/Pure/Isar/element.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/Isar/element.ML Tue Apr 18 22:24:48 2023 +0200
@@ -207,7 +207,7 @@
SOME C =>
let
val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
- val insts = (TVars.empty, Vars.make [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]);
+ val insts = (TVars.empty, Vars.make1 (Term.dest_Var C, Thm.cterm_of ctxt thesis));
val th' = Thm.instantiate insts th;
in (th', true) end
| NONE => (th, false));
--- a/src/Pure/Tools/rule_insts.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/Tools/rule_insts.ML Tue Apr 18 22:24:48 2023 +0200
@@ -280,7 +280,7 @@
fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT));
val revcut_rl' =
Drule.revcut_rl |> Drule.instantiate_normalize
- (TVars.empty, Vars.make [(var "V", cvar ("V", maxidx + 1)), (var "W", cvar ("W", maxidx + 1))]);
+ (TVars.empty, Vars.make2 (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}
--- a/src/Pure/conjunction.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/conjunction.ML Tue Apr 18 22:24:48 2023 +0200
@@ -102,7 +102,7 @@
fun intr tha thb =
Thm.implies_elim
(Thm.implies_elim
- (Thm.instantiate (TVars.empty, Vars.make [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)])
+ (Thm.instantiate (TVars.empty, Vars.make2 (vA, Thm.cprop_of tha) (vB, Thm.cprop_of thb))
conjunctionI)
tha)
thb;
@@ -111,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 (TVars.empty, Vars.make [(vA, A), (vB, B)]);
+ val inst = Thm.instantiate (TVars.empty, Vars.make2 (vA, A) (vB, B));
in
(Thm.implies_elim (inst conjunctionD1) th,
Thm.implies_elim (inst conjunctionD2) th)
--- a/src/Pure/drule.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/drule.ML Tue Apr 18 22:24:48 2023 +0200
@@ -599,7 +599,7 @@
val cT = Thm.ctyp_of_cterm ct;
val T = Thm.typ_of cT;
in
- Thm.instantiate (TVars.make [((("'a", 0), []), cT)], Vars.make [((("x", 0), T), ct)]) termI
+ Thm.instantiate (TVars.make1 ((("'a", 0), []), cT), Vars.make1 ((("x", 0), T), ct)) termI
end;
fun dest_term th =
--- a/src/Pure/ex/Guess.thy Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/ex/Guess.thy Tue Apr 18 22:24:48 2023 +0200
@@ -174,7 +174,7 @@
[] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])]
|> snd
|> Proof.refine_singleton (Method.Basic (fn _ => fn _ => CONTEXT_TACTIC
- (PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(guess, Thm.cterm_of ctxt thesis)]))
+ (PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make1 (guess, Thm.cterm_of ctxt thesis)))
THEN Goal.conjunction_tac 1
THEN resolve_tac ctxt [Drule.termI] 1)))
end;
--- a/src/Pure/goal.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/goal.ML Tue Apr 18 22:24:48 2023 +0200
@@ -57,7 +57,7 @@
-------- (init)
C \<Longrightarrow> #C
*)
-fun init C = Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), C)]) Drule.protectI;
+fun init C = Thm.instantiate (TVars.empty, Vars.make1 ((("A", 0), propT), C)) Drule.protectI;
(*
A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> C
--- a/src/Pure/raw_simplifier.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/Pure/raw_simplifier.ML Tue Apr 18 22:24:48 2023 +0200
@@ -1216,7 +1216,7 @@
val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
val eq' =
Thm.implies_elim
- (Thm.instantiate (TVars.empty, Vars.make [(vA, prem), (vB, lhs), (vC, rhs)])
+ (Thm.instantiate (TVars.empty, Vars.make3 (vA, prem) (vB, lhs) (vC, rhs))
Drule.imp_cong)
(Thm.implies_intr prem eq);
in
@@ -1228,10 +1228,10 @@
in
Thm.transitive
(Thm.transitive
- (Thm.instantiate (TVars.empty, Vars.make [(vA, prem'), (vB, prem), (vC, concl)])
+ (Thm.instantiate (TVars.empty, Vars.make3 (vA, prem') (vB, prem) (vC, concl))
Drule.swap_prems_eq)
eq')
- (Thm.instantiate (TVars.empty, Vars.make [(vA, prem), (vB, prem''), (vC, concl)])
+ (Thm.instantiate (TVars.empty, Vars.make3 (vA, prem) (vB, prem'') (vC, concl))
Drule.swap_prems_eq)
end
end
--- a/src/ZF/Tools/cartprod.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/ZF/Tools/cartprod.ML Tue Apr 18 22:24:48 2023 +0200
@@ -107,7 +107,7 @@
in
remove_split ctxt
(Drule.instantiate_normalize (TVars.empty,
- Vars.make [((v, \<^Type>\<open>i\<close> --> T2), Thm.cterm_of ctxt newt)]) rl)
+ Vars.make1 ((v, \<^Type>\<open>i\<close> --> T2), Thm.cterm_of ctxt newt)) rl)
end
| split_rule_var _ (t,T,rl) = rl;
--- a/src/ZF/Tools/inductive_package.ML Tue Apr 18 21:47:40 2023 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Apr 18 22:24:48 2023 +0200
@@ -506,7 +506,7 @@
val inst =
case elem_frees of [_] => I
| _ => Drule.instantiate_normalize (TVars.empty,
- Vars.make [((("x", 1), \<^Type>\<open>i\<close>), Thm.global_cterm_of thy4 elem_tuple)]);
+ Vars.make1 ((("x", 1), \<^Type>\<open>i\<close>), Thm.global_cterm_of thy4 elem_tuple));
(*strip quantifier and the implication*)
val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));