# HG changeset patch # User wenzelm # Date 1737580939 -3600 # Node ID 6f2bcdfa9a1940cb4b5dd6cf44b8771f364a7500 # Parent 02d9844ff8928f4bbb3f328cc743c8b99b78f752 misc tuning: more concise operations on prems (without change of exceptions); discontinue odd clone Drule.cprems_of (see also 991a3feaf270); diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Wed Jan 22 21:35:05 2025 +0100 +++ b/src/CCL/Wfd.thy Wed Jan 22 22:22:19 2025 +0100 @@ -424,9 +424,9 @@ | get_bno l n (Bound m) = (m-length(l),n) (* Not a great way of identifying induction hypothesis! *) -fun could_IH x = Term.could_unify(x,hd (Thm.prems_of @{thm rcallT})) orelse - Term.could_unify(x,hd (Thm.prems_of @{thm rcall2T})) orelse - Term.could_unify(x,hd (Thm.prems_of @{thm rcall3T})) +fun could_IH x = Term.could_unify(x,hd (Thm.take_prems_of 1 @{thm rcallT})) orelse + Term.could_unify(x,hd (Thm.take_prems_of 1 @{thm rcall2T})) orelse + Term.could_unify(x,hd (Thm.take_prems_of 1 @{thm rcall3T})) fun IHinst tac rls = SUBGOAL (fn (Bi,i) => let val bvs = bvars Bi [] diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Analysis/measurable.ML --- a/src/HOL/Analysis/measurable.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Analysis/measurable.ML Wed Jan 22 22:22:19 2025 +0100 @@ -125,7 +125,7 @@ | _ => raise (TERM ("not a measurability predicate", [t]))) fun not_measurable_prop n thm = - if length (Thm.prems_of thm) < n then false + if Thm.nprems_of thm < n then false else (case nth_hol_goal thm n of \<^Const_>\Set.member _ for _ \<^Const_>\sets _ for _\\ => false diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Analysis/normarith.ML --- a/src/HOL/Analysis/normarith.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Analysis/normarith.ML Wed Jan 22 22:22:19 2025 +0100 @@ -359,7 +359,7 @@ val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts') 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 cps = map (swap o Thm.dest_equals) (Thm.cprems_of 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]) diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/HOL.thy Wed Jan 22 22:22:19 2025 +0100 @@ -2177,7 +2177,7 @@ fun wrong_prem \<^Const_>\All _ for \Abs (_, _, t)\\ = wrong_prem t | wrong_prem (Bound _) = true | wrong_prem _ = false; - val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of); + val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.take_prems_of 1); fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp]; in fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt]; diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Library/cconv.ML --- a/src/HOL/Library/cconv.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Library/cconv.ML Wed Jan 22 22:22:19 2025 +0100 @@ -131,7 +131,7 @@ |> Thm.cterm_of ctxt end val rule = abstract_rule_thm x - val inst = Thm.match (hd (Drule.cprems_of rule), mk_concl eq) + val inst = Thm.match (hd (Thm.take_cprems_of 1 rule), mk_concl eq) val gen = (Names.empty, Names.make1_set (#1 (dest_Free v))) in (Drule.instantiate_normalize inst rule OF [Drule.generalize gen eq]) diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Jan 22 22:22:19 2025 +0100 @@ -12,7 +12,7 @@ (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) fun gen_res_inst_tac_term ctxt instf tyinst tinst elim th i st = let - val cgoal = nth (cprems_of st) (i - 1); + val cgoal = nth (Thm.cprems_of st) (i - 1); val maxidx = Thm.maxidx_of_cterm cgoal; val j = maxidx + 1; val tyinst' = map (apfst (Logic.incr_tvar j)) tyinst; diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Jan 22 22:22:19 2025 +0100 @@ -147,7 +147,7 @@ eta_contract_cterm (Conjunction.mk_conjunction_balanced objs)); fun first_order_mrs ths th = ths MRS - Thm.instantiate (first_order_matchs (cprems_of th) (map Thm.cprop_of ths)) th; + Thm.instantiate (first_order_matchs (Thm.cprems_of th) (map Thm.cprop_of ths)) th; fun prove_strong_ind s avoids lthy = let @@ -531,7 +531,7 @@ | NONE => fold_rev (NominalDatatype.mk_perm []) pis x) | x => x) o HOLogic.dest_Trueprop o Thm.prop_of) case_hyps)); val inst = Thm.first_order_match (Thm.dest_arg - (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj); + (Drule.strip_imp_concl (hd (Thm.cprems_of case_hyp))), obj); val th = Goal.prove ctxt3 [] [] (Thm.term_of concl) (fn {context = ctxt4, ...} => resolve_tac ctxt4 [Thm.instantiate inst case_hyp] 1 THEN diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Wed Jan 22 22:22:19 2025 +0100 @@ -289,7 +289,7 @@ (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) fun finite_guess_tac_i tactical ctxt i st = - let val goal = nth (cprems_of st) (i - 1) + let val goal = nth (Thm.cprems_of st) (i - 1) in case Envir.eta_contract (Logic.strip_assums_concl (Thm.term_of goal)) of _ $ (Const (\<^const_name>\finite\, _) $ (Const (\<^const_name>\Nominal.supp\, T) $ x)) => @@ -329,7 +329,7 @@ (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *) fun fresh_guess_tac_i tactical ctxt i st = let - val goal = nth (cprems_of st) (i - 1) + val goal = nth (Thm.cprems_of st) (i - 1) val fin_supp = Proof_Context.get_thms ctxt "fin_supp" val fresh_atm = Proof_Context.get_thms ctxt "fresh_atm" val ctxt1 = ctxt addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Jan 22 22:22:19 2025 +0100 @@ -545,7 +545,7 @@ val assms_tac = let val assms' = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms in fold (curry (op ORELSE')) (map (fn thm => - funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' assume_tac ctxt) + funpow (Thm.nprems_of thm) (fn tac => tac THEN' assume_tac ctxt) (rtac ctxt thm)) assms') (etac ctxt FalseE) end; diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Wed Jan 22 22:22:19 2025 +0100 @@ -176,7 +176,7 @@ val psimp = import sum_psimp_eq val (simp, restore_cond) = - case cprems_of psimp of + case Thm.cprems_of psimp of [] => (psimp, I) | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) | _ => raise General.Fail "Too many conditions" diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Jan 22 22:22:19 2025 +0100 @@ -156,7 +156,7 @@ val concl_pat = Drule.strip_imp_concl (Thm.cprop_of rule) val insts = Thm.first_order_match (concl_pat, cprop) val rule = Drule.instantiate_normalize insts rule - val prop = hd (Thm.prems_of rule) + val prop = hd (Thm.take_prems_of 1 rule) in case mono_eq_prover ctxt prop of SOME thm => SOME (thm RS rule) @@ -233,7 +233,7 @@ val preprocessed_thm = preprocess ctxt0 thm val (fixed_thm, ctxt1) = ctxt0 |> yield_singleton (apfst snd oo Variable.import true) preprocessed_thm - val assms = cprems_of fixed_thm + val assms = Thm.cprems_of fixed_thm val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add val (prems, ctxt2) = ctxt1 |> fold_map Thm.assume_hyps assms val ctxt3 = ctxt2 |> Context.proof_map (fold add_transfer_rule prems) @@ -386,7 +386,7 @@ val rel_fun = prove_rel ctxt rsp_thm (rty, qty) val rep_abs_thm = [quot_thm, rel_fun] MRSL @{thm Quotient_rep_abs_eq} in - case mono_eq_prover ctxt (hd (Thm.prems_of rep_abs_thm)) of + case mono_eq_prover ctxt (hd (Thm.take_prems_of 1 rep_abs_thm)) of SOME mono_eq_thm => let val rep_abs_eq = mono_eq_thm RS rep_abs_thm diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Jan 22 22:22:19 2025 +0100 @@ -637,7 +637,7 @@ let fun prove_extra_assms thm = let - val assms = cprems_of thm + val assms = Thm.cprems_of thm fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm)) in diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Jan 22 22:22:19 2025 +0100 @@ -427,7 +427,7 @@ fun reduce_Domainp ctxt rules thm = let - val goal = thm |> Thm.prems_of |> hd + val goal = hd (Thm.take_prems_of 1 thm) val var = goal |> HOLogic.dest_Trueprop |> dest_comb |> snd |> dest_Var val reduced_assm = reduce_goal [var] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt @@ -439,7 +439,7 @@ let fun reduce_first_assm ctxt rules thm = let - val goal = thm |> Thm.prems_of |> hd + val goal = hd (Thm.take_prems_of 1 thm) val reduced_assm = reduce_goal [] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt in diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Wed Jan 22 22:22:19 2025 +0100 @@ -463,7 +463,7 @@ | _ => false val inst_distr_rule = rewr_imp distr_rule ctm - val extra_assms = filter_out is_POS_or_NEG (cprems_of inst_distr_rule) + val extra_assms = filter_out is_POS_or_NEG (Thm.cprems_of inst_distr_rule) val proved_assms = map_interrupt prove_assm extra_assms in Option.map (curry op OF inst_distr_rule) proved_assms @@ -491,7 +491,7 @@ case distr_rule of NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ()) | SOME distr_rule => - map (gen_merge_transfer_relations quotients ctxt0) (cprems_of distr_rule) + map (gen_merge_transfer_relations quotients ctxt0) (Thm.cprems_of distr_rule) MRSL distr_rule end else @@ -504,7 +504,7 @@ val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm) val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm val result = (map (gen_merge_transfer_relations quotients ctxt0) - (cprems_of distr_rule)) MRSL distr_rule + (Thm.cprems_of distr_rule)) MRSL distr_rule val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def) in Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.combination_conv diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Wed Jan 22 22:22:19 2025 +0100 @@ -558,7 +558,7 @@ #> let_simps ? rewrite_rule ctxt @{thms Let_def [abs_def]} fun make_nnf simp_options ctxt th = - (case Thm.prems_of th of + (case Thm.take_prems_of 1 th of [] => th |> presimplify simp_options ctxt |> make_nnf1 ctxt | _ => raise THM ("make_nnf: premises in argument", 0, [th])); diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/Old_Datatype/old_datatype_aux.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Wed Jan 22 22:22:19 2025 +0100 @@ -154,7 +154,7 @@ val params = Logic.strip_params goal; val tname = dest_Type_name (#2 (hd (rev params))); val exhaustion = Thm.lift_rule cgoal (exh_thm_of tname); - val prem' = hd (Thm.prems_of exhaustion); + val prem' = hd (Thm.take_prems_of 1 exhaustion); val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem')); val exhaustion' = infer_instantiate ctxt diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Wed Jan 22 22:22:19 2025 +0100 @@ -385,7 +385,7 @@ fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) = let - val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.prems_of exhaustion))); + val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.take_prems_of 1 exhaustion))); val ctxt = Proof_Context.init_global thy; val exhaustion' = exhaustion |> infer_instantiate ctxt [(#1 (dest_Var lhs), Thm.cterm_of ctxt (Free ("x", T)))]; diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Jan 22 22:22:19 2025 +0100 @@ -237,7 +237,7 @@ val prems2 = maps (dest_conjunct_prem o rewrite_rule ctxt2 tuple_rew_rules) prems1 val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) - (take nargs (Thm.prems_of case_th)) + (Thm.take_prems_of nargs case_th) val case_th' = Thm.instantiate (TVars.empty, Vars.make (inst_of_matches pats)) case_th OF replicate nargs @{thm refl} @@ -325,7 +325,7 @@ fun set_elim thm = let - val name = dest_Const_name (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.prems_of thm))))) + val name = dest_Const_name (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.take_prems_of 1 thm))))) in PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm)))))))) end diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/cnf.ML --- a/src/HOL/Tools/cnf.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/cnf.ML Wed Jan 22 22:22:19 2025 +0100 @@ -106,7 +106,7 @@ (* becomes "[..., A1, ..., An] |- B" *) fun prems_to_hyps thm = fold (fn cprem => fn thm' => - Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm + Thm.implies_elim thm' (Thm.assume cprem)) (Thm.cprems_of thm) thm in (* [...] |- ~(x1 | ... | xn) ==> False *) (@{thm cnf.clause2raw_notE} OF [clause]) diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/coinduction.ML --- a/src/HOL/Tools/coinduction.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/coinduction.ML Wed Jan 22 22:22:19 2025 +0100 @@ -71,7 +71,7 @@ val (instT, inst) = Thm.match (thm_concl, concl); 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 + val xs = hd (Thm.take_prems_of 1 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; val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Jan 22 22:22:19 2025 +0100 @@ -372,7 +372,7 @@ let val vs' = rename (map (apply2 (fst o fst o dest_Var)) (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop - (hd (Thm.prems_of (hd inducts))))), nparms))) vs; + (hd (Thm.take_prems_of 1 (hd inducts))))), nparms))) vs; val rs = indrule_realizer thy induct raw_induct rsets params' (vs' @ Ps) rec_names rss' intrs dummies; val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r @@ -505,7 +505,7 @@ fun err () = error "ind_realizer: bad rule"; val sets = (case HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of thm)) of - [_] => [pred_of (HOLogic.dest_Trueprop (hd (Thm.prems_of thm)))] + [_] => [pred_of (HOLogic.dest_Trueprop (hd (Thm.take_prems_of 1 thm)))] | xs => map (pred_of o fst o HOLogic.dest_imp) xs) handle TERM _ => err () | List.Empty => err (); in diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/HOL/Tools/record.ML Wed Jan 22 22:22:19 2025 +0100 @@ -1504,7 +1504,7 @@ val (x, ca) = (case rev (drop (length params) ys) of [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop - (hd (rev (Logic.strip_assums_hyp (hd (Thm.prems_of rule')))))))), true) + (hd (rev (Logic.strip_assums_hyp (hd (Thm.take_prems_of 1 rule')))))))), true) | [x] => (head_of x, false)); val rule'' = infer_instantiate ctxt diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/Provers/hypsubst.ML Wed Jan 22 22:22:19 2025 +0100 @@ -169,7 +169,7 @@ val (ixn, T) = dest_Var (Term.head_of (Data.dest_Trueprop (Logic.strip_assums_concl (Thm.prop_of rl')))); val (v1, v2) = Data.dest_eq (Data.dest_Trueprop - (Logic.strip_assums_concl (hd (Thm.prems_of rl')))); + (Logic.strip_assums_concl (hd (Thm.take_prems_of 1 rl')))); val (Ts, V) = split_last (Term.binder_types T); val u = fold_rev Term.abs (ps @ [("x", U)]) diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/Pure/Isar/rule_cases.ML Wed Jan 22 22:22:19 2025 +0100 @@ -423,7 +423,7 @@ fun prep_rule n th = let val th' = Thm.permute_prems 0 n th; - val prems = take (Thm.nprems_of th' - n) (Drule.cprems_of th'); + val prems = Thm.take_cprems_of (Thm.nprems_of th' - n) th'; val th'' = Drule.implies_elim_list th' (map Thm.assume prems); in (prems, (n, th'')) end; diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/Pure/drule.ML --- a/src/Pure/drule.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/Pure/drule.ML Wed Jan 22 22:22:19 2025 +0100 @@ -12,7 +12,6 @@ val list_implies: cterm list * cterm -> cterm val strip_imp_prems: cterm -> cterm list val strip_imp_concl: cterm -> cterm - val cprems_of: thm -> cterm list val forall_intr_list: cterm list -> thm -> thm val forall_elim_list: cterm list -> thm -> thm val lift_all: Proof.context -> cterm -> thm -> thm @@ -127,9 +126,6 @@ Const ("Pure.imp", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct) | _ => ct); -(*The premises of a theorem, as a cterm list*) -val cprems_of = strip_imp_prems o Thm.cprop_of; - fun certify t = Thm.global_cterm_of (Context.the_global_context ()) t; val implies = certify Logic.implies; diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/Pure/search.ML --- a/src/Pure/search.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/Pure/search.ML Wed Jan 22 22:22:19 2025 +0100 @@ -129,7 +129,7 @@ let val np' = Thm.nprems_of st; (*rgd' calculation assumes tactic operates on subgoal 1*) - val rgd' = not (has_vars (hd (Thm.prems_of st))); + val rgd' = not (has_vars (hd (Thm.take_prems_of 1 st))); val k' = k + np' - np + 1; (*difference in # of subgoals, +1*) in if k' + np' >= bnd then depth (bnd, Int.min (inc, k' + np' + 1 - bnd)) qs diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/Tools/IsaPlanner/isand.ML --- a/src/Tools/IsaPlanner/isand.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/Tools/IsaPlanner/isand.ML Wed Jan 22 22:22:19 2025 +0100 @@ -102,7 +102,7 @@ fun hide_other_goals th = let (* tl beacuse fst sg is the goal we are interested in *) - val cprems = tl (Drule.cprems_of th); + val cprems = tl (Thm.cprems_of th); val aprems = map Thm.assume cprems; in (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, cprems) end; diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/Tools/induct.ML --- a/src/Tools/induct.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/Tools/induct.ML Wed Jan 22 22:22:19 2025 +0100 @@ -120,7 +120,7 @@ in -fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty => +fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.take_prems_of 1 thm)))) handle List.Empty => raise THM ("No variables in major premise of rule", 0, [thm]); val left_var_concl = concl_var hd; diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Wed Jan 22 21:35:05 2025 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Wed Jan 22 22:22:19 2025 +0100 @@ -97,7 +97,7 @@ |> (if exh then #exhaustion else #induct) |> Thm.transfer thy; val \<^Const_>\mem for \Var(ixn,_)\ _\ = - (case Thm.prems_of rule of + (case Thm.take_prems_of 1 rule of [] => error "induction is not available for this datatype" | major::_ => \<^dest_judgment> major) in @@ -124,7 +124,7 @@ val constructors = map (head_of o const_of o \<^dest_judgment> o Thm.prop_of) case_eqns; - val \<^Const_>\mem for _ data\ = \<^dest_judgment> (hd (Thm.prems_of elim)); + val \<^Const_>\mem for _ data\ = \<^dest_judgment> (hd (Thm.take_prems_of 1 elim)); val Const(big_rec_name, _) = head_of data;