src/HOL/Typerep.thy

--- a/src/HOL/Typerep.thy	Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Typerep.thy	Sun Jun 23 21:16:07 2013 +0200
@@ -87,11 +87,9 @@
   "HOL.equal (x :: typerep) x \<longleftrightarrow> True"
   by (fact equal_refl)
 
-code_type typerep
-  (Eval "Term.typ")
-
-code_const Typerep
-  (Eval "Term.Type/ (_, _)")
+code_printing
+  type_constructor typerep \<rightharpoonup> (Eval) "Term.typ"
+| constant Typerep \<rightharpoonup> (Eval) "Term.Type/ (_, _)"
 
 code_reserved Eval Term