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