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>