--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Sep 25 14:11:48 2020 +0100
@@ -326,7 +326,7 @@
shows "odd (card {s\<in>simplices. (rl ` s = {..Suc n})})"
proof (rule kuhn_counting_lemma)
have finite_s[simp]: "\<And>s. s \<in> simplices \<Longrightarrow> finite s"
- by (metis add_is_0 zero_neq_numeral card_infinite assms(3))
+ by (metis add_is_0 zero_neq_numeral card.infinite assms(3))
let ?F = "{f. \<exists>s\<in>simplices. face f s}"
have F_eq: "?F = (\<Union>s\<in>simplices. \<Union>a\<in>s. {s - {a}})"