changeset 52435 | 6646bb548c6b |
parent 52143 | 36ffe23b25f8 |
child 56243 | 2e10a36b8d46 |
--- 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