# HG changeset patch # User wenzelm # Date 1681849488 -7200 # Node ID dd222e2af01a2e4e817d8406e4a6d9c669593615 # Parent 35a1788dd6f9bd6e9dab8ec6c0a24692e3adf9b0 tuned; diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Decision_Procs/ferrante_rackoff.ML --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Library/cconv.ML --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Library/old_recdef.ML --- 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; diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Nominal/nominal_datatype.ML --- 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>\rev\, permT --> permT) $ pi))]) th] 1 THEN + Vars.make1 ((("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,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)) diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Nominal/nominal_fresh_fun.ML --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Real_Asymp/multiseries_expansion.ML --- 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' diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Statespace/distinct_tree_prover.ML --- 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>\Node\, nT) $ l $ x $ d $ r) ct dist_thm = let diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Argo/argo_real.ML --- 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 = diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Argo/argo_tactic.ML --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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 = diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- 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); diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Function/induction_schema.ML --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Function/partial_function.ML --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Function/relation.ML --- 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 = diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Meson/meson.ML --- 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; diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Meson/meson_clausify.ML --- 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_>\Trueprop for \Var (v as (_, \<^Type>\bool\))\\ => - Thm.instantiate (TVars.empty, Vars.make [(v, cfalse)]) th + Thm.instantiate (TVars.empty, Vars.make1 (v, cfalse)) th | Var (v as (_, \<^Type>\prop\)) => - Thm.instantiate (TVars.empty, Vars.make [(v, ctp_false)]) th + Thm.instantiate (TVars.empty, Vars.make1 (v, ctp_false)) th | _ => th) diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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' diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Qelim/cooper.ML --- 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 = diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Quickcheck/random_generators.ML --- 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>\0::natural\ 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)) diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/Quotient/quotient_tacs.ML --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/SMT/smt_normalize.ML --- 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 = diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/numeral.ML --- 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>\uminus\; val uminus = cterm_of (Const (\<^const_name>\uminus\, 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/numeral_simprocs.ML --- 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>\Trueprop\ (Thm.apply \<^cterm>\Not\ diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/semiring_normalizer.ML --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/HOL/Tools/split_rule.ML --- 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; diff -r 35a1788dd6f9 -r dd222e2af01a src/Provers/Arith/fast_lin_arith.ML --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/Isar/class_declaration.ML --- 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, [])))], []); diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/Isar/element.ML --- 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)); diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/Tools/rule_insts.ML --- 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} diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/conjunction.ML --- 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) diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/drule.ML --- 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 = diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/ex/Guess.thy --- 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; diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/goal.ML --- 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 \ #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 \ ... \ An \ C diff -r 35a1788dd6f9 -r dd222e2af01a src/Pure/raw_simplifier.ML --- 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 diff -r 35a1788dd6f9 -r dd222e2af01a src/ZF/Tools/cartprod.ML --- 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>\i\ --> T2), Thm.cterm_of ctxt newt)]) rl) + Vars.make1 ((v, \<^Type>\i\ --> T2), Thm.cterm_of ctxt newt)) rl) end | split_rule_var _ (t,T,rl) = rl; diff -r 35a1788dd6f9 -r dd222e2af01a src/ZF/Tools/inductive_package.ML --- 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>\i\), Thm.global_cterm_of thy4 elem_tuple)]); + Vars.make1 ((("x", 1), \<^Type>\i\), 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}));