--- a/src/HOL/Library/Cardinality.thy Thu Jun 18 09:07:28 2020 +0000
+++ b/src/HOL/Library/Cardinality.thy Thu Jun 18 09:07:29 2020 +0000
@@ -217,7 +217,7 @@
instantiation int :: card_UNIV begin
definition "finite_UNIV = Phantom(int) False"
definition "card_UNIV = Phantom(int) 0"
-instance by intro_classes (simp_all add: card_UNIV_int_def finite_UNIV_int_def infinite_UNIV_int)
+instance by intro_classes (simp_all add: card_UNIV_int_def finite_UNIV_int_def)
end
instantiation natural :: card_UNIV begin