--- a/src/HOL/Inductive.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Inductive.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -467,7 +467,7 @@
   show "inj_on ?h A"
   proof -
     from inj1 X_sub have on_X: "inj_on f X"
-      by (rule subset_inj_on)
+      by (rule inj_on_subset)
 
     have on_X_compl: "inj_on g' (A - X)"
       unfolding g'_def X_compl