1.1 --- a/src/HOL/Library/Numeral_Type.thy	Sun Feb 17 22:56:54 2013 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Feb 18 08:52:23 2013 +0100
     1.3 @@ -447,9 +447,7 @@
     1.4  
     1.5  instantiation bit0 and bit1 :: ("{finite,card_UNIV}") card_UNIV begin
     1.6  definition "card_UNIV = Phantom('a bit0) (2 * of_phantom (card_UNIV :: 'a card_UNIV))"
     1.7 -definition
     1.8 -  "card_UNIV = Phantom('a bit1) (let ca = of_phantom (card_UNIV :: 'a card_UNIV)
     1.9 -  in if ca \<noteq> 0 then 1 + 2 * ca else 2 * ca)"
    1.10 +definition "card_UNIV = Phantom('a bit1) (1 + 2 * of_phantom (card_UNIV :: 'a card_UNIV))"
    1.11  instance by intro_classes (simp_all add: card_UNIV_bit0_def card_UNIV_bit1_def card_UNIV)
    1.12  end
    1.13