src/HOL/Library/Cardinality.thy
changeset 42247 12fe41a92cd5
parent 42245 29e3967550d5
child 44142 8e27e0177518
     1.1 --- a/src/HOL/Library/Cardinality.thy	Wed Apr 06 13:27:59 2011 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Wed Apr 06 13:33:46 2011 +0200
     1.3 @@ -34,12 +34,11 @@
     1.4  
     1.5  translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
     1.6  
     1.7 -typed_print_translation {*
     1.8 -let
     1.9 -  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
    1.10 -    Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ show_sorts T;
    1.11 -in [(@{const_syntax card}, card_univ_tr')]
    1.12 -end
    1.13 +typed_print_translation (advanced) {*
    1.14 +  let
    1.15 +    fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T, _]))] =
    1.16 +      Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T;
    1.17 +  in [(@{const_syntax card}, card_univ_tr')] end
    1.18  *}
    1.19  
    1.20  lemma card_unit [simp]: "CARD(unit) = 1"