diff -r c5d1a01d2d6c -r d7d90ed4c74e src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Sep 25 14:11:48 2020 +0100
@@ -417,7 +417,7 @@
 proof (induction n arbitrary: S)
   case 0
   then show ?case
-    by (metis all_not_in_conv card_empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
+    by (metis all_not_in_conv card.empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
 next
   case (Suc n)
   show ?case