src/HOL/Library/Cardinality.thy
changeset 52147 9943f8067f11
parent 52143 36ffe23b25f8
child 53015 a1119cf551e8
--- a/src/HOL/Library/Cardinality.thy	Sat May 25 17:13:34 2013 +0200
+++ b/src/HOL/Library/Cardinality.thy	Sat May 25 17:40:44 2013 +0200
@@ -43,9 +43,9 @@
 
 translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
 
-typed_print_translation {*
+print_translation {*
   let
-    fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] =
+    fun card_univ_tr' ctxt [Const (@{const_syntax UNIV}, Type (_, [T]))] =
       Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
   in [(@{const_syntax card}, card_univ_tr')] end
 *}