tuned;

--- 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
 *}

--- a/src/HOL/Library/Numeral_Type.thy	Sat May 25 17:13:34 2013 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Sat May 25 17:40:44 2013 +0200
@@ -519,7 +519,8 @@
       | bit_tr' b _ = raise Match;
   in
    [(@{type_syntax bit0}, K (bit_tr' 0)),
-    (@{type_syntax bit1}, K (bit_tr' 1))] end;
+    (@{type_syntax bit1}, K (bit_tr' 1))]
+  end;
 *}
 
 subsection {* Examples *}

--- a/src/HOL/Library/Phantom_Type.thy	Sat May 25 17:13:34 2013 +0200
+++ b/src/HOL/Library/Phantom_Type.thy	Sat May 25 17:40:44 2013 +0200
@@ -29,10 +29,10 @@
 
 typed_print_translation {*
   let
-    fun phantom_tr' ctxt 
-        (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
-          list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
-    | phantom_tr' _ _ _ = raise Match;
+    fun phantom_tr' ctxt (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
+          list_comb
+            (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
+      | phantom_tr' _ _ _ = raise Match;
   in [(@{const_syntax phantom}, phantom_tr')] end
 *}