1.1 --- a/src/HOL/Tools/typedef.ML	Mon Oct 13 20:24:24 2014 +0200
     1.2 +++ b/src/HOL/Tools/typedef.ML	Mon Oct 13 20:25:10 2014 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val transform_info: morphism -> info -> info
     1.5    val get_info: Proof.context -> string -> info list
     1.6    val get_info_global: theory -> string -> info list
     1.7 -  val interpretation: (string -> theory -> theory) -> theory -> theory
     1.8 +  val interpretation: (string -> local_theory -> local_theory) -> theory -> theory
     1.9    val add_typedef: bool -> binding * (string * sort) list * mixfix ->
    1.10      term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
    1.11    val add_typedef_global: bool -> binding * (string * sort) list * mixfix ->
    1.12 @@ -71,18 +71,18 @@
    1.13  
    1.14  (* global interpretation *)
    1.15  
    1.16 -structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
    1.17 +structure Typedef_Plugin = Plugin(type T = string);
    1.18 +
    1.19 +val typedef_plugin = Plugin_Name.declare_setup @{binding typedef};
    1.20  
    1.21 -fun with_repaired_path f name thy =
    1.22 -  thy
    1.23 -  |> Sign.root_path
    1.24 -  |> Sign.add_path (Long_Name.qualifier name)
    1.25 -  |> f name
    1.26 -  |> Sign.restore_naming thy;
    1.27 -
    1.28 -fun interpretation f = Typedef_Interpretation.interpretation (with_repaired_path f);
    1.29 -
    1.30 -val _ = Theory.setup Typedef_Interpretation.init;
    1.31 +fun interpretation f =
    1.32 +  Typedef_Plugin.interpretation typedef_plugin
    1.33 +    (fn name => fn lthy =>
    1.34 +      lthy
    1.35 +      |> Local_Theory.map_naming
    1.36 +          (Name_Space.root_path #> Name_Space.add_path (Long_Name.qualifier name))
    1.37 +      |> f name
    1.38 +      |> Local_Theory.restore_naming lthy);
    1.39  
    1.40  
    1.41  (* primitive typedef axiomatization -- for fresh typedecl *)
    1.42 @@ -229,7 +229,7 @@
    1.43          lthy2
    1.44          |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.45            (fn phi => put_info full_name (transform_info phi info))
    1.46 -        |> Local_Theory.background_theory (Typedef_Interpretation.data full_name)
    1.47 +        |> Typedef_Plugin.data Plugin_Name.default_filter full_name
    1.48          |> pair (full_name, info)
    1.49        end;
    1.50  

     2.1 --- a/src/HOL/Typerep.thy	Mon Oct 13 20:24:24 2014 +0200
     2.2 +++ b/src/HOL/Typerep.thy	Mon Oct 13 20:25:10 2014 +0200
     2.3 @@ -71,7 +71,7 @@
     2.4  in
     2.5  
     2.6  add_typerep @{type_name fun}
     2.7 -#> Typedef.interpretation ensure_typerep
     2.8 +#> Typedef.interpretation (Local_Theory.background_theory o ensure_typerep)
     2.9  #> Code.datatype_interpretation (ensure_typerep o fst)
    2.10  #> Code.abstype_interpretation (ensure_typerep o fst)
    2.11