src/HOL/Library/Numeral_Type.thy

   unfolding type_definition.card [OF type_definition_num0]
   by simp
 
 lemma card_num1 [simp]: "CARD(num1) = 1"
   unfolding type_definition.card [OF type_definition_num1]
-  by (simp only: card_unit)
+  by (simp only: card_UNIV_unit)
 
 lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)"
   unfolding type_definition.card [OF type_definition_bit0]
   by simp