--- 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