# HG changeset patch
# User wenzelm
# Date 1413224664 -7200
# Node ID 2b9485a2d1524f48771846d37bcf9d2c4a97edd6
# Parent  8d4aebb9e327900207cc35c011bee99eda59483f
module Interpretation is superseded by Plugin;

diff -r 8d4aebb9e327 -r 2b9485a2d152 src/HOL/Tools/Old_Datatype/old_datatype_data.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Oct 13 19:34:10 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Oct 13 20:24:24 2014 +0200
@@ -237,28 +237,26 @@
 
 (** abstract theory extensions relative to a datatype characterisation **)
 
-structure Datatype_Interpretation = Interpretation
-(
-  type T = Old_Datatype_Aux.config * string list;
-  val eq: T * T -> bool = eq_snd (op =);
-);
+structure Old_Datatype_Plugin = Plugin(type T = Old_Datatype_Aux.config * string list);
+
+val old_datatype_plugin = Plugin_Name.declare_setup @{binding old_datatype};
 
-fun with_repaired_path f config (type_names as name :: _) thy =
-  thy
-  |> Sign.root_path
-  |> Sign.add_path (Long_Name.qualifier name)
-  |> f config type_names
-  |> Sign.restore_naming thy;
+fun interpretation f =
+  Old_Datatype_Plugin.interpretation old_datatype_plugin
+    (fn (config, type_names as name :: _) =>
+      Local_Theory.background_theory (fn thy =>
+        thy
+        |> Sign.root_path
+        |> Sign.add_path (Long_Name.qualifier name)
+        |> f config type_names
+        |> Sign.restore_naming thy));
 
-fun interpretation f = Datatype_Interpretation.interpretation (uncurry (with_repaired_path f));
-val interpretation_data = Datatype_Interpretation.data;
-
+fun interpretation_data x =
+  Named_Target.theory_init #>
+  Old_Datatype_Plugin.data Plugin_Name.default_filter x #>
+  Local_Theory.exit_global;
 
 
-(** setup theory **)
-
-val _ = Theory.setup Datatype_Interpretation.init;
-
 open Old_Datatype_Aux;
 
 end;