misc tuning: more concise operations on prems (without change of exceptions);
discontinue odd clone Drule.cprems_of (see also 991a3feaf270);
--- 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 []
--- 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_>\<open>Set.member _ for _ \<^Const_>\<open>sets _ for _\<close>\<close> => false
--- 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])
--- 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_>\<open>All _ for \<open>Abs (_, _, t)\<close>\<close> = 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];
--- 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])
--- 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;
--- 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
--- 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>\<open>finite\<close>, _) $ (Const (\<^const_name>\<open>Nominal.supp\<close>, 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
--- 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;
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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]));
--- 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
--- 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)))];
--- 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
--- 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])
--- 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
--- 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
--- 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
--- 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)])
--- 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;
--- 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;
--- 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
--- 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;
--- 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;
--- 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_>\<open>mem for \<open>Var(ixn,_)\<close> _\<close> =
- (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_>\<open>mem for _ data\<close> = \<^dest_judgment> (hd (Thm.prems_of elim));
+ val \<^Const_>\<open>mem for _ data\<close> = \<^dest_judgment> (hd (Thm.take_prems_of 1 elim));
val Const(big_rec_name, _) = head_of data;