src/HOL/Library/Cardinality.thy

--- a/src/HOL/Library/Cardinality.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Library/Cardinality.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -236,7 +236,7 @@
 instance
   by standard
     (auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff
-      type_definition.univ [OF type_definition_integer] infinite_UNIV_int
+      type_definition.univ [OF type_definition_integer]
       dest!: finite_imageD intro: inj_onI)
 end