src/HOL/Typerep.thy
changeset 66330 dcb3e6bdc00a
parent 63352 4eaf35781b23
child 69593 3dda49e08b9d
--- a/src/HOL/Typerep.thy	Thu Aug 03 12:50:01 2017 +0200
+++ b/src/HOL/Typerep.thy	Thu Aug 03 12:50:02 2017 +0200
@@ -72,8 +72,7 @@
 
 add_typerep @{type_name fun}
 #> Typedef.interpretation (Local_Theory.background_theory o ensure_typerep)
-#> Code.datatype_interpretation (ensure_typerep o fst)
-#> Code.abstype_interpretation (ensure_typerep o fst)
+#> Code.type_interpretation ensure_typerep
 
 end
 \<close>