--- a/src/HOL/Combinatorics/Permutations.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Combinatorics/Permutations.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -797,7 +797,7 @@
   from \<open>p permutes S\<close> have "inj p"
     by (rule permutes_inj)
   then have "inj_on p S"
-    by (auto intro: subset_inj_on)
+    by (auto intro: inj_on_subset)
   then have "F g (p ` S) = F (g \<circ> p) S"
     by (rule reindex)
   moreover from \<open>p permutes S\<close> have "p ` S = S"