src/HOL/Library/Cardinality.thy

 definition "finite_UNIV = Phantom(integer) False"
 definition "card_UNIV = Phantom(integer) 0"
 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
 
 instantiation list :: (type) card_UNIV begin
 definition "finite_UNIV = Phantom('a list) False"