src/HOL/Library/Numeral_Type.thy

--- a/src/HOL/Library/Numeral_Type.thy	Fri May 08 19:20:00 2009 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Sat May 09 07:25:22 2009 +0200
@@ -55,7 +55,7 @@
   unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus)
 
 lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)"
-  unfolding insert_None_conv_UNIV [symmetric]
+  unfolding UNIV_option_conv
   apply (subgoal_tac "(None::'a option) \<notin> range Some")
   apply (simp add: card_image)
   apply fast