# HG changeset patch
# User wenzelm
# Date 1413224710 -7200
# Node ID 5963cdbad9265ee29df1eadef1f969b236bbe278
# Parent  2b9485a2d1524f48771846d37bcf9d2c4a97edd6
module Interpretation is superseded by Plugin;

diff -r 2b9485a2d152 -r 5963cdbad926 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon Oct 13 20:24:24 2014 +0200
+++ b/src/HOL/Tools/typedef.ML	Mon Oct 13 20:25:10 2014 +0200
@@ -15,7 +15,7 @@
   val transform_info: morphism -> info -> info
   val get_info: Proof.context -> string -> info list
   val get_info_global: theory -> string -> info list
-  val interpretation: (string -> theory -> theory) -> theory -> theory
+  val interpretation: (string -> local_theory -> local_theory) -> theory -> theory
   val add_typedef: bool -> binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
   val add_typedef_global: bool -> binding * (string * sort) list * mixfix ->
@@ -71,18 +71,18 @@
 
 (* global interpretation *)
 
-structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
+structure Typedef_Plugin = Plugin(type T = string);
+
+val typedef_plugin = Plugin_Name.declare_setup @{binding typedef};
 
-fun with_repaired_path f name thy =
-  thy
-  |> Sign.root_path
-  |> Sign.add_path (Long_Name.qualifier name)
-  |> f name
-  |> Sign.restore_naming thy;
-
-fun interpretation f = Typedef_Interpretation.interpretation (with_repaired_path f);
-
-val _ = Theory.setup Typedef_Interpretation.init;
+fun interpretation f =
+  Typedef_Plugin.interpretation typedef_plugin
+    (fn name => fn lthy =>
+      lthy
+      |> Local_Theory.map_naming
+          (Name_Space.root_path #> Name_Space.add_path (Long_Name.qualifier name))
+      |> f name
+      |> Local_Theory.restore_naming lthy);
 
 
 (* primitive typedef axiomatization -- for fresh typedecl *)
@@ -229,7 +229,7 @@
         lthy2
         |> Local_Theory.declaration {syntax = false, pervasive = true}
           (fn phi => put_info full_name (transform_info phi info))
-        |> Local_Theory.background_theory (Typedef_Interpretation.data full_name)
+        |> Typedef_Plugin.data Plugin_Name.default_filter full_name
         |> pair (full_name, info)
       end;
 
diff -r 2b9485a2d152 -r 5963cdbad926 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Mon Oct 13 20:24:24 2014 +0200
+++ b/src/HOL/Typerep.thy	Mon Oct 13 20:25:10 2014 +0200
@@ -71,7 +71,7 @@
 in
 
 add_typerep @{type_name fun}
-#> Typedef.interpretation ensure_typerep
+#> Typedef.interpretation (Local_Theory.background_theory o ensure_typerep)
 #> Code.datatype_interpretation (ensure_typerep o fst)
 #> Code.abstype_interpretation (ensure_typerep o fst)