src/HOL/Library/Cardinality.thy

--- a/src/HOL/Library/Cardinality.thy	Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Library/Cardinality.thy	Sat May 25 15:37:53 2013 +0200
@@ -43,7 +43,7 @@
 
 translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
 
-typed_print_translation (advanced) {*
+typed_print_translation {*
   let
     fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] =
       Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T