# HG changeset patch
# User wenzelm
# Date 1349276360 -7200
# Node ID b8a710806de997d653730b84c7912298ad2b08e3
# Parent  c517d900805a28a434401ef4da5fe771b582bf10
recovered print translation after 'a => bool to 'a set change;

diff -r c517d900805a -r b8a710806de9 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Wed Oct 03 16:43:41 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Wed Oct 03 16:59:20 2012 +0200
@@ -45,8 +45,8 @@
 
 typed_print_translation (advanced) {*
   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;
+    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
 *}