src/HOL/Library/Numeral_Type.thy
changeset 30506 105ad9a68e51
parent 30242 aea5d7fa7ef5
child 30663 0b6aff7451b2
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Fri Mar 13 07:30:47 2009 -0700
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Mar 13 07:35:18 2009 -0700
     1.3 @@ -36,7 +36,7 @@
     1.4  
     1.5  typed_print_translation {*
     1.6  let
     1.7 -  fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] =
     1.8 +  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_,[T,_]))] =
     1.9      Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
    1.10  in [(@{const_syntax card}, card_univ_tr')]
    1.11  end