diff -r 9f07e961a2b0 -r 6f0e85e16d84 src/HOL/Library/Perm.thy
--- a/src/HOL/Library/Perm.thy	Fri Sep 25 16:32:41 2020 +0200
+++ b/src/HOL/Library/Perm.thy	Fri Sep 25 17:13:12 2020 +0100
@@ -365,7 +365,7 @@
   then obtain B b where "affected f = insert b B"
     by blast
   with finite_affected [of f] have "card (affected f) \<ge> 1"
-    by (simp add: card_insert)
+    by (simp add: card.insert_remove)
   case False then have "order f a = 1"
     by (simp add: order_eq_one_iff)
   with \<open>card (affected f) \<ge> 1\<close> show ?thesis