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