diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -1538,7 +1538,7 @@
   also have "\<dots> = Suc (card ({k \<in> M. k < Suc i} - {0}))"
     by (force intro: arg_cong [where f=card])
   also have "\<dots> = card (insert 0 ({k \<in> M. k < Suc i} - {0}))"
-    by (simp add: card_insert)
+    by (simp add: card.insert_remove)
   also have "... = card {k \<in> M. k < Suc i}"
     using assms
     by (force simp add: intro: arg_cong [where f=card])