# HG changeset patch
# User huffman
# Date 1228065000 -3600
# Node ID 4ed4b8b1988d1513e8b2446a65a73dfd12b9b433
# Parent  88b8cc1a29839eb5b3d5736e7d5baf28c630b5fb
fix typed print translation for card UNIV

diff -r 88b8cc1a2983 -r 4ed4b8b1988d src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Sun Nov 30 16:00:16 2008 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Sun Nov 30 18:10:00 2008 +0100
@@ -52,13 +52,13 @@
 
 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
 
-translations "CARD(t)" => "CONST card (UNIV \<Colon> t set)"
+translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
 
 typed_print_translation {*
 let
-  fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T]))] =
+  fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] =
     Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
-in [("card", card_univ_tr')]
+in [(@{const_syntax card}, card_univ_tr')]
 end
 *}
 
@@ -241,5 +241,5 @@
 
 lemma "CARD(0) = 0" by simp
 lemma "CARD(17) = 17" by simp
-  
+
 end