# HG changeset patch
# User huffman
# Date 1236954918 25200
# Node ID 105ad9a68e51ac8602b321832779e49019db979a
# Parent  110e59507eec584c9b4ece213b2c5a8b04b26998
fix typed print translation for CARD('a)

diff -r 110e59507eec -r 105ad9a68e51 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Fri Mar 13 07:30:47 2009 -0700
+++ b/src/HOL/Library/Numeral_Type.thy	Fri Mar 13 07:35:18 2009 -0700
@@ -36,7 +36,7 @@
 
 typed_print_translation {*
 let
-  fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] =
+  fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_,[T,_]))] =
     Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
 in [(@{const_syntax card}, card_univ_tr')]
 end