diff -r 15bba1fb39d1 -r 29e3967550d5 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Library/Cardinality.thy	Wed Apr 06 12:58:13 2011 +0200
@@ -37,7 +37,7 @@
 typed_print_translation {*
 let
   fun card_univ_tr' show_sorts _ [Const (@{const_syntax UNIV}, Type(_, [T, _]))] =
-    Syntax.const @{syntax_const "_type_card"} $ Syntax.term_of_typ show_sorts T;
+    Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ show_sorts T;
 in [(@{const_syntax card}, card_univ_tr')]
 end
 *}