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