diff -r cf2cccf17d6d -r b037fd9016fa src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Tue Feb 26 20:38:17 2008 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Tue Feb 26 20:38:18 2008 +0100
@@ -63,26 +63,26 @@
 *}
 
 lemma card_unit: "CARD(unit) = 1"
-  unfolding univ_unit by simp
+  unfolding UNIV_unit by simp
 
 lemma card_bool: "CARD(bool) = 2"
-  unfolding univ_bool by simp
+  unfolding UNIV_bool by simp
 
 lemma card_prod: "CARD('a::finite \<times> 'b::finite) = CARD('a) * CARD('b)"
-  unfolding univ_prod by (simp only: card_cartesian_product)
+  unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
 
 lemma card_sum: "CARD('a::finite + 'b::finite) = CARD('a) + CARD('b)"
-  unfolding univ_sum by (simp only: finite card_Plus)
+  unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
 
 lemma card_option: "CARD('a::finite option) = Suc CARD('a)"
-  unfolding univ_option
+  unfolding insert_None_conv_UNIV [symmetric]
   apply (subgoal_tac "(None::'a option) \<notin> range Some")
   apply (simp add: finite card_image)
   apply fast
   done
 
 lemma card_set: "CARD('a::finite set) = 2 ^ CARD('a)"
-  unfolding univ_set
+  unfolding Pow_UNIV [symmetric]
   by (simp only: card_Pow finite numeral_2_eq_2)