src/HOL/Library/Numeral_Type.thy
changeset 28920 4ed4b8b1988d
parent 27487 c8a6ce181805
child 29025 8c8859c0d734
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Sun Nov 30 16:00:16 2008 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sun Nov 30 18:10:00 2008 +0100
     1.3 @@ -52,13 +52,13 @@
     1.4  
     1.5  syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
     1.6  
     1.7 -translations "CARD(t)" => "CONST card (UNIV \<Colon> t set)"
     1.8 +translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
     1.9  
    1.10  typed_print_translation {*
    1.11  let
    1.12 -  fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T]))] =
    1.13 +  fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] =
    1.14      Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
    1.15 -in [("card", card_univ_tr')]
    1.16 +in [(@{const_syntax card}, card_univ_tr')]
    1.17  end
    1.18  *}
    1.19  
    1.20 @@ -241,5 +241,5 @@
    1.21  
    1.22  lemma "CARD(0) = 0" by simp
    1.23  lemma "CARD(17) = 17" by simp
    1.24 -  
    1.25 +
    1.26  end