src/HOL/Typerep.thy
changeset 58662 5963cdbad926
parent 58310 91ea607a34d8
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Typerep.thy	Mon Oct 13 20:24:24 2014 +0200
     1.2 +++ b/src/HOL/Typerep.thy	Mon Oct 13 20:25:10 2014 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  in
     1.5  
     1.6  add_typerep @{type_name fun}
     1.7 -#> Typedef.interpretation ensure_typerep
     1.8 +#> Typedef.interpretation (Local_Theory.background_theory o ensure_typerep)
     1.9  #> Code.datatype_interpretation (ensure_typerep o fst)
    1.10  #> Code.abstype_interpretation (ensure_typerep o fst)
    1.11