diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Library/Perm.thy
--- a/src/HOL/Library/Perm.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/Perm.thy	Fri Sep 25 14:11:48 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