src/HOL/Library/Cardinality.thy
changeset 49689 b8a710806de9
parent 48176 3d9c1ddb9f47
child 49948 744934b818c7
     1.1 --- a/src/HOL/Library/Cardinality.thy	Wed Oct 03 16:43:41 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Wed Oct 03 16:59:20 2012 +0200
     1.3 @@ -45,8 +45,8 @@
     1.4  
     1.5  typed_print_translation (advanced) {*
     1.6    let
     1.7 -    fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T, _]))] =
     1.8 -      Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T;
     1.9 +    fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] =
    1.10 +      Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
    1.11    in [(@{const_syntax card}, card_univ_tr')] end
    1.12  *}
    1.13