diff -r ba8f5e4fa336 -r d1dce7d0731c src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Fri Nov 23 21:09:30 2007 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Fri Nov 23 21:09:32 2007 +0100
@@ -52,7 +52,7 @@
 
 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
 
-translations "CARD(t)" => "card (UNIV::t set)"
+translations "CARD(t)" => "CONST card (UNIV \<Colon> t set)"
 
 typed_print_translation {*
 let
@@ -239,8 +239,6 @@
 
 subsection {* Examples *}
 
-term "TYPE(10)"
-
 lemma "CARD(0) = 0" by simp
 lemma "CARD(17) = 17" by simp