# 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;