src/HOL/Library/Cardinality.thy
changeset 42245 29e3967550d5
parent 37653 847e95ca9b0a
child 42247 12fe41a92cd5
     1.1 --- a/src/HOL/Library/Cardinality.thy	Wed Apr 06 12:55:53 2011 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Wed Apr 06 12:58:13 2011 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  typed_print_translation {*
     1.5  let
     1.6    fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
     1.7 -    Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
     1.8 +    Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ show_sorts T;
     1.9  in [(@{const_syntax card}, card_univ_tr')]
    1.10  end
    1.11  *}