# HG changeset patch
# User wenzelm
# Date 1413230260 -7200
# Node ID d2a7b443ceb277155bad15a4ca77b80086f74f59
# Parent  7f14d5d9b933f458cf26d7cdf1a1a74107a532e4# Parent  9e34267662674fb1da7de0b712a35b24f0dafa6f
merged

diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Oct 13 21:57:40 2014 +0200
@@ -500,8 +500,10 @@
 
 \item
 The @{text "plugins"} option indicates which plugins should be enabled
-(@{text only}) or disabled (@{text del}). Wildcards (``@{text "*"}'') are
-allowed (e.g., @{text "quickcheck_*"}). By default, all plugins are enabled.
+(@{text only}) or disabled (@{text del}). Some plugin names are defined
+as indirection to a group of sub-plugins (notably @{text "quickcheck"}
+based on @{text quickcheck_random}, @{text quickcheck_exhaustive}, \dots).
+By default, all plugins are enabled.
 
 \item
 The @{text "discs_sels"} option indicates that discriminators and selectors
@@ -2794,7 +2796,7 @@
 For example:
 *}
 
-    datatype (plugins del: code "quickcheck_*") color = Red | Black
+    datatype (plugins del: code "quickcheck") color = Red | Black
 
 
 subsection {* Code Generator
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Ctr_Sugar.thy
--- a/src/HOL/Ctr_Sugar.thy	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Ctr_Sugar.thy	Mon Oct 13 21:57:40 2014 +0200
@@ -37,7 +37,6 @@
   "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
   by blast+
 
-ML_file "Tools/Ctr_Sugar/local_interpretation.ML"
 ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
 ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
 ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Enum.thy	Mon Oct 13 21:57:40 2014 +0200
@@ -493,7 +493,7 @@
 
 text {* We define small finite types for use in Quickcheck *}
 
-datatype (plugins only: code "quickcheck*" extraction) finite_1 =
+datatype (plugins only: code "quickcheck" extraction) finite_1 =
   a\<^sub>1
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
@@ -596,7 +596,7 @@
 declare [[simproc del: finite_1_eq]]
 hide_const (open) a\<^sub>1
 
-datatype (plugins only: code "quickcheck*" extraction) finite_2 =
+datatype (plugins only: code "quickcheck" extraction) finite_2 =
   a\<^sub>1 | a\<^sub>2
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
@@ -711,7 +711,7 @@
 
 hide_const (open) a\<^sub>1 a\<^sub>2
 
-datatype (plugins only: code "quickcheck*" extraction) finite_3 =
+datatype (plugins only: code "quickcheck" extraction) finite_3 =
   a\<^sub>1 | a\<^sub>2 | a\<^sub>3
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
@@ -838,7 +838,7 @@
 
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
 
-datatype (plugins only: code "quickcheck*" extraction) finite_4 =
+datatype (plugins only: code "quickcheck" extraction) finite_4 =
   a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
@@ -940,7 +940,7 @@
 
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
 
-datatype (plugins only: code "quickcheck*" extraction) finite_5 =
+datatype (plugins only: code "quickcheck" extraction) finite_5 =
   a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/HOL.thy	Mon Oct 13 21:57:40 2014 +0200
@@ -40,6 +40,25 @@
   #> Case_Product.setup
 *}
 
+ML \<open>Plugin_Name.declare_setup @{binding extraction}\<close>
+
+ML \<open>
+  Plugin_Name.declare_setup @{binding quickcheck_random};
+  Plugin_Name.declare_setup @{binding quickcheck_exhaustive};
+  Plugin_Name.declare_setup @{binding quickcheck_bounded_forall};
+  Plugin_Name.declare_setup @{binding quickcheck_full_exhaustive};
+  Plugin_Name.declare_setup @{binding quickcheck_narrowing};
+\<close>
+ML \<open>
+  Plugin_Name.define_setup @{binding quickcheck}
+   [@{plugin quickcheck_exhaustive},
+    @{plugin quickcheck_random},
+    @{plugin quickcheck_bounded_forall},
+    @{plugin quickcheck_full_exhaustive},
+    @{plugin quickcheck_narrowing}]
+\<close>
+
+
 subsection {* Primitive logic *}
 
 subsubsection {* Core syntax *}
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Library/bnf_axiomatization.ML
--- a/src/HOL/Library/bnf_axiomatization.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -17,9 +17,11 @@
 open BNF_Util
 open BNF_Def
 
-fun prepare_decl prepare_constraint prepare_typ plugins raw_vars b mx user_mapb user_relb user_witTs
-  lthy =
+fun prepare_decl prepare_plugins prepare_constraint prepare_typ
+    raw_plugins raw_vars b mx user_mapb user_relb user_witTs lthy =
   let
+   val plugins = prepare_plugins lthy raw_plugins;
+
    fun prepare_type_arg (set_opt, (ty, c)) =
       let val s = fst (dest_TFree (prepare_typ lthy ty)) in
         (set_opt, (s, prepare_constraint lthy c))
@@ -95,12 +97,12 @@
     (bnf, register_bnf plugins key bnf lthy')
   end;
 
-val bnf_axiomatization = prepare_decl (K I) (K I);
+val bnf_axiomatization = prepare_decl (K I) (K I) (K I);
 
 fun read_constraint _ NONE = @{sort type}
   | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
 
-val bnf_axiomatization_cmd = prepare_decl read_constraint Syntax.read_typ;
+val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ;
 
 val parse_witTs =
   @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
@@ -109,7 +111,7 @@
   @{keyword "]"} || Scan.succeed [];
 
 val parse_bnf_axiomatization_options =
-  Scan.optional (@{keyword "("} |-- parse_plugins --| @{keyword ")"}) (K true);
+  Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"}) (K (K true));
 
 val parse_bnf_axiomatization =
   parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding --
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -17,8 +17,7 @@
   val transfer_bnf: theory -> bnf -> bnf
   val bnf_of: Proof.context -> string -> bnf option
   val bnf_of_global: theory -> string -> bnf option
-  val bnf_interpretation: string -> (bnf -> theory -> theory) ->
-    (bnf -> local_theory -> local_theory) -> theory -> theory
+  val bnf_interpretation: string -> (bnf -> local_theory -> local_theory) -> theory -> theory
   val interpret_bnf: (string -> bool) -> bnf -> local_theory -> local_theory
   val register_bnf_raw: string -> bnf -> local_theory -> local_theory
   val register_bnf: (string -> bool) -> string -> bnf -> local_theory -> local_theory
@@ -1514,18 +1513,13 @@
     (key, goals, wit_goalss, after_qed, lthy, one_step_defs)
   end;
 
-structure BNF_Interpretation = Local_Interpretation
-(
-  type T = bnf;
-  val eq: T * T -> bool = op = o pairself T_of_bnf;
-);
+structure BNF_Plugin = Plugin(type T = bnf);
 
-fun with_transfer_bnf g bnf thy = g (transfer_bnf thy bnf) thy;
+fun bnf_interpretation name f =
+  BNF_Plugin.interpretation name
+    (fn bnf => fn lthy => f (transfer_bnf (Proof_Context.theory_of lthy) bnf) lthy);
 
-fun bnf_interpretation name =
-  BNF_Interpretation.interpretation name o with_transfer_bnf;
-
-val interpret_bnf = BNF_Interpretation.data;
+val interpret_bnf = BNF_Plugin.data;
 
 fun register_bnf_raw key bnf =
   Local_Theory.declaration {syntax = false, pervasive = true}
@@ -1557,9 +1551,10 @@
   end) o prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs
     raw_csts;
 
-fun bnf_cmd (raw_csts, plugins) =
+fun bnf_cmd (raw_csts, raw_plugins) =
   (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
   let
+    val plugins = raw_plugins lthy;
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
     fun mk_triv_wit_thms tac set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
@@ -1619,9 +1614,7 @@
          Scan.repeat1 (Scan.unless (Parse.reserved "rel" ||
            Parse.reserved "plugins") Parse.term)) [] --
        Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) --
-       Scan.optional parse_plugins (K true)
+       Scan.optional Plugin_Name.parse_filter (K Plugin_Name.default_filter)
        >> bnf_cmd);
 
-val _ = Context.>> (Context.map_theory BNF_Interpretation.init);
-
 end;
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -67,7 +67,7 @@
   val fp_sugar_of_global: theory -> string -> fp_sugar option
   val fp_sugars_of: Proof.context -> fp_sugar list
   val fp_sugars_of_global: theory -> fp_sugar list
-  val fp_sugars_interpretation: string -> (fp_sugar list -> theory -> theory) ->
+  val fp_sugars_interpretation: string ->
     (fp_sugar list -> local_theory -> local_theory)-> theory -> theory
   val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
   val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
@@ -316,18 +316,14 @@
 fun co_induct_of (i :: _) = i;
 fun strong_co_induct_of [_, s] = s;
 
-structure FP_Sugar_Interpretation = Local_Interpretation
-(
-  type T = fp_sugar list;
-  val eq: T * T -> bool = op = o pairself (map #T);
-);
+structure FP_Sugar_Plugin = Plugin(type T = fp_sugar list);
 
-fun with_transfer_fp_sugars g fp_sugars thy = g (map (transfer_fp_sugar thy) fp_sugars) thy;
+fun fp_sugars_interpretation name f =
+  FP_Sugar_Plugin.interpretation name
+    (fn fp_sugars => fn lthy =>
+      f (map (transfer_fp_sugar (Proof_Context.theory_of lthy)) fp_sugars) lthy);
 
-fun fp_sugars_interpretation name =
-  FP_Sugar_Interpretation.interpretation name o with_transfer_fp_sugars;
-
-val interpret_fp_sugars = FP_Sugar_Interpretation.data;
+val interpret_fp_sugars = FP_Sugar_Plugin.data;
 
 fun register_fp_sugars_raw fp_sugars =
   fold (fn fp_sugar as {T = Type (s, _), ...} =>
@@ -984,7 +980,7 @@
             |> map Thm.close_derivation
         end;
 
-      val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+      val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
 
       val anonymous_notes =
         [(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
@@ -1417,7 +1413,7 @@
 
     val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
 
-    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+    val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
   in
     ((induct_thms, induct_thm, mk_induct_attrs ctrss),
      (rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs))
@@ -1828,11 +1824,12 @@
      (corec_sel_thmsss, simp_attrs))
   end;
 
-fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
-    ((plugins, discs_sels0), specs) no_defs_lthy =
+fun define_co_datatypes prepare_plugins prepare_constraint prepare_typ prepare_term fp construct_fp
+    ((raw_plugins, discs_sels0), specs) no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
 
+    val plugins = prepare_plugins no_defs_lthy raw_plugins;
     val discs_sels = discs_sels0 orelse fp = Greatest_FP;
 
     val nn = length specs;
@@ -2010,7 +2007,7 @@
     val fpTs = map (domain_type o fastype_of) dtors;
     val fpBTs = map B_ify_T fpTs;
 
-    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+    val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
 
     val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
     val ns = map length ctr_Tsss;
@@ -2375,10 +2372,11 @@
     timer; lthy''
   end;
 
-fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) x;
+fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) (K I) x;
 
 fun co_datatype_cmd x =
-  define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x;
+  define_co_datatypes Plugin_Name.make_filter Typedecl.read_constraint
+    Syntax.parse_typ Syntax.parse_term x;
 
 val parse_ctr_arg =
   @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"}
@@ -2395,6 +2393,4 @@
 
 fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
 
-val _ = Theory.setup FP_Sugar_Interpretation.init;
-
 end;
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -176,7 +176,7 @@
         set_inducts = []}}
   end;
 
-val _ = Theory.setup (map_local_theory (fn lthy =>
+val _ = Theory.setup (Named_Target.theory_map (fn lthy =>
   fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy))
     [fp_sugar_of_sum, fp_sugar_of_prod] lthy));
 
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -451,10 +451,8 @@
   end;
 
 fun interpretation name prefs f =
-  let val new_f = new_interpretation_of prefs f in
-    Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
-    #> fp_sugars_interpretation name new_f (Local_Theory.background_theory o new_f)
-  end;
+  Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
+  #> fp_sugars_interpretation name (Local_Theory.background_theory o new_interpretation_of prefs f);
 
 val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
 
@@ -501,7 +499,7 @@
     |> snd
   end;
 
-val datatype_compat_global = map_local_theory o datatype_compat;
+val datatype_compat_global = Named_Target.theory_map o datatype_compat;
 
 fun datatype_compat_cmd raw_fpT_names lthy =
   let
@@ -529,7 +527,8 @@
   in
     (fpT_names,
      thy
-     |> map_local_theory (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs))
+     |> Named_Target.theory_map
+       (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs))
      |> not (member (op =) prefs Keep_Nesting) ? perhaps (try (datatype_compat_global fpT_names)))
   end;
 
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -7,7 +7,6 @@
 
 signature BNF_LFP_SIZE =
 sig
-  val size_plugin: string
   val register_size: string -> string -> thm list -> thm list -> local_theory -> local_theory
   val register_size_global: string -> string -> thm list -> thm list -> theory -> theory
   val size_of: Proof.context -> string -> (string * (thm list * thm list)) option
@@ -22,8 +21,6 @@
 open BNF_Def
 open BNF_FP_Def_Sugar
 
-val size_plugin = "size";
-
 val size_N = "size_";
 
 val rec_o_mapN = "rec_o_map";
@@ -396,7 +393,7 @@
     end
   | generate_datatype_size _ lthy = lthy;
 
-val _ = Theory.setup (fp_sugars_interpretation size_plugin
-  (map_local_theory o generate_datatype_size) generate_datatype_size);
+val size_plugin = Plugin_Name.declare_setup @{binding size};
+val _ = Theory.setup (fp_sugars_interpretation size_plugin generate_datatype_size);
 
 end;
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -103,7 +103,6 @@
   val parse_type_args_named_constrained: (binding option * (string * string option)) list parser
   val parse_map_rel_bindings: (binding * binding) parser
 
-  val map_local_theory: (local_theory -> local_theory) -> theory -> theory
   val typedef: binding * (string * sort) list * mixfix -> term ->
     (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
 end;
@@ -141,8 +140,6 @@
     >> (fn ps => fold extract_map_rel ps no_map_rel)
   || Scan.succeed no_map_rel;
 
-fun map_local_theory f = Named_Target.theory_init #> f #> Local_Theory.exit_global;
-
 fun typedef (b, Ts, mx) set opt_morphs tac lthy =
   let
     (*Work around loss of qualification in "typedef" axioms by replicating it in the name*)
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -7,8 +7,6 @@
 
 signature CTR_SUGAR =
 sig
-  val code_plugin: string
-
   type ctr_sugar =
     {T: typ,
      ctrs: term list,
@@ -46,7 +44,7 @@
   val ctr_sugars_of_global: theory -> ctr_sugar list
   val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
   val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
-  val ctr_sugar_interpretation: string -> (ctr_sugar -> theory -> theory) ->
+  val ctr_sugar_interpretation: string ->
     (ctr_sugar -> local_theory -> local_theory) -> theory -> theory
   val interpret_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
   val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory
@@ -72,14 +70,16 @@
   val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
 
   type ctr_options = (string -> bool) * bool
+  type ctr_options_cmd = (Proof.context -> string -> bool) * bool
 
   val fake_local_theory_for_sel_defaults: (binding * typ) list -> Proof.context -> Proof.context
   val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     ((ctr_options * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
     ctr_sugar * local_theory
   val default_ctr_options: ctr_options
+  val default_ctr_options_cmd: ctr_options_cmd
   val parse_bound_term: (binding * string) parser
-  val parse_ctr_options: ctr_options parser
+  val parse_ctr_options: ctr_options_cmd parser
   val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a) ctr_spec parser
   val parse_sel_default_eqs: string list parser
 end;
@@ -91,8 +91,6 @@
 open Ctr_Sugar_Tactics
 open Ctr_Sugar_Code
 
-val code_plugin = "code";
-
 type ctr_sugar =
   {T: typ,
    ctrs: term list,
@@ -183,18 +181,14 @@
 val ctr_sugar_of_case = ctr_sugar_of_case_generic o Context.Proof;
 val ctr_sugar_of_case_global = ctr_sugar_of_case_generic o Context.Theory;
 
-structure Ctr_Sugar_Interpretation = Local_Interpretation
-(
-  type T = ctr_sugar;
-  val eq: T * T -> bool = op = o pairself #ctrs;
-);
+structure Ctr_Sugar_Plugin = Plugin(type T = ctr_sugar);
 
-fun with_transfer_ctr_sugar g ctr_sugar thy = g (transfer_ctr_sugar thy ctr_sugar) thy;
+fun ctr_sugar_interpretation name f =
+  Ctr_Sugar_Plugin.interpretation name
+    (fn ctr_sugar => fn lthy =>
+      f (transfer_ctr_sugar (Proof_Context.theory_of lthy) ctr_sugar) lthy);
 
-fun ctr_sugar_interpretation name =
-  Ctr_Sugar_Interpretation.interpretation name o with_transfer_ctr_sugar;
-
-val interpret_ctr_sugar = Ctr_Sugar_Interpretation.data;
+val interpret_ctr_sugar = Ctr_Sugar_Plugin.data;
 
 fun register_ctr_sugar_raw (ctr_sugar as {T = Type (s, _), ...}) =
   Local_Theory.declaration {syntax = false, pervasive = true}
@@ -210,7 +204,7 @@
     else
       thy
       |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
-      |> Ctr_Sugar_Interpretation.data_global plugins ctr_sugar
+      |> Named_Target.theory_map (Ctr_Sugar_Plugin.data plugins ctr_sugar)
   end;
 
 val isN = "is_";
@@ -364,9 +358,15 @@
 fun ctr_of_ctr_spec ((_, ctr), _) = ctr;
 fun args_of_ctr_spec (_, args) = args;
 
-fun prepare_free_constructors prep_term ((((plugins, discs_sels), raw_case_binding), ctr_specs),
-    sel_default_eqs) no_defs_lthy =
+val code_plugin = Plugin_Name.declare_setup @{binding code};
+
+fun prepare_free_constructors prep_plugins prep_term
+    ((((raw_plugins, discs_sels), raw_case_binding), ctr_specs),
+      sel_default_eqs) no_defs_lthy =
   let
+    val plugins = prep_plugins no_defs_lthy raw_plugins;
+
+
     (* TODO: sanity checks on arguments *)
 
     val raw_ctrs = map ctr_of_ctr_spec ctr_specs;
@@ -1056,24 +1056,27 @@
 
 fun free_constructors tacss = (fn (goalss, after_qed, lthy) =>
   map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
-  |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I);
+  |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I) (K I);
 
 val free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
   Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
-  prepare_free_constructors Syntax.read_term;
+  prepare_free_constructors Plugin_Name.make_filter Syntax.read_term;
 
 val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
 
-type ctr_options = (string -> bool) * bool;
+type ctr_options = Plugin_Name.filter * bool;
+type ctr_options_cmd = (Proof.context -> Plugin_Name.filter) * bool;
 
-val default_ctr_options = (K true, false) : ctr_options;
+val default_ctr_options : ctr_options = (Plugin_Name.default_filter, false);
+val default_ctr_options_cmd : ctr_options_cmd = (K Plugin_Name.default_filter, false);
 
 val parse_ctr_options =
   Scan.optional (@{keyword "("} |-- Parse.list1
-        (parse_plugins >> (apfst o K) || Parse.reserved "discs_sels" >> (apsnd o K o K true)) --|
+        (Plugin_Name.parse_filter >> (apfst o K) ||
+         Parse.reserved "discs_sels" >> (apsnd o K o K true)) --|
       @{keyword ")"}
-      >> (fn fs => fold I fs default_ctr_options))
-    default_ctr_options;
+      >> (fn fs => fold I fs default_ctr_options_cmd))
+    default_ctr_options_cmd;
 
 fun parse_ctr_spec parse_ctr parse_arg =
   parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg;
@@ -1088,6 +1091,4 @@
        -- parse_sel_default_eqs
      >> free_constructors_cmd);
 
-val _ = Theory.setup Ctr_Sugar_Interpretation.init;
-
 end;
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -71,7 +71,6 @@
   val standard_binding: binding
   val parse_binding_colon: binding parser
   val parse_opt_binding_colon: binding parser
-  val parse_plugins: (string -> bool) parser
 
   val ss_only: thm list -> Proof.context -> Proof.context
 
@@ -87,18 +86,6 @@
 structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
 struct
 
-fun match_entire_string pat s =
-  let
-    fun match [] [] = true
-      | match [] _ = false
-      | match (ps as #"*" :: ps') cs =
-        match ps' cs orelse (not (null cs) andalso match ps (tl cs))
-      | match _ [] = false
-      | match (p :: ps) (c :: cs) = p = c andalso match ps cs;
-  in
-    match (String.explode pat) (String.explode s)
-  end;
-
 fun map_prod f g (x, y) = (f x, g y);
 
 fun seq_conds f n k xs =
@@ -262,12 +249,6 @@
 val parse_binding_colon = Parse.binding --| @{keyword ":"};
 val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
 
-val parse_plugins =
-  Parse.reserved "plugins" |--
-    ((Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --| @{keyword ":"}
-     -- Scan.repeat (Parse.short_ident || Parse.string))
-  >> (fn (modif, pats) => modif o member (uncurry match_entire_string o swap) pats);
-
 fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
 
 (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/Ctr_Sugar/local_interpretation.ML
--- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Mon Oct 13 18:55:05 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(*  Title:      HOL/Tools/Ctr_Sugar/local_interpretation.ML
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Generic interpretation of local theory data -- ad hoc. Based on
-
-    Title:      Pure/interpretation.ML
-    Author:     Florian Haftmann and Makarius
-*)
-
-signature LOCAL_INTERPRETATION =
-sig
-  type T
-  val result: theory -> T list
-  val interpretation: string -> (T -> theory -> theory) -> (T -> local_theory -> local_theory) ->
-    theory -> theory
-  val data: (string -> bool) -> T -> local_theory -> local_theory
-  val data_global: (string -> bool) -> T -> theory -> theory
-  val init: theory -> theory
-end;
-
-functor Local_Interpretation(type T val eq: T * T -> bool): LOCAL_INTERPRETATION =
-struct
-
-type T = T;
-
-structure Interp = Theory_Data
-(
-  type T =
-    ((Name_Space.naming * (string -> bool)) * T) list
-    * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * (string * stamp))
-       * ((Name_Space.naming * (string -> bool)) * T) list) list;
-  val empty = ([], []);
-  val extend = I;
-  fun merge ((data1, interps1), (data2, interps2)) : T =
-    (Library.merge (eq_snd eq) (data1, data2),
-     AList.join (eq_snd (op =)) (K (Library.merge (eq_snd eq))) (interps1, interps2));
-);
-
-val result = map snd o fst o Interp.get;
-
-fun consolidate_common g_or_f lift_lthy thy thy_or_lthy =
-  let
-    val (data, interps) = Interp.get thy;
-
-    fun unfinished_of ((gf, (name, _)), data') =
-      (g_or_f gf,
-       if eq_list (eq_snd eq) (data', data) then
-         []
-       else
-         subtract (eq_snd eq) data' data
-         |> map_filter (fn ((naming, keep), x) => if keep name then SOME (naming, x) else NONE));
-
-    val unfinished = map unfinished_of interps;
-    val finished = map (apsnd (K data)) interps;
-  in
-    if forall (null o #2) unfinished then
-      NONE
-    else
-      SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
-        |> lift_lthy (Interp.put (data, finished)))
-  end;
-
-fun consolidate lthy =
-  consolidate_common (fn (_, g) => fn (_, x) => g x) Local_Theory.background_theory
-    (Proof_Context.theory_of lthy) lthy;
-
-fun consolidate_global thy =
-  consolidate_common (fn (f, _) => fn (naming, x) => fn thy =>
-    thy |> Sign.map_naming (K naming) |> f x |> Sign.restore_naming thy) I thy thy;
-
-fun interpretation name g f =
-  Interp.map (apsnd (cons (((g, f), (name, stamp ())), []))) #> perhaps consolidate_global;
-
-fun data keep x =
-  Local_Theory.background_theory
-    (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
-  #> perhaps consolidate;
-
-fun data_global keep x =
-  (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
-  #> perhaps consolidate_global;
-
-val init = Theory.at_begin consolidate_global;
-
-end;
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/Lifting/lifting_bnf.ML
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -6,7 +6,6 @@
 
 signature LIFTING_BNF =
 sig
-  val lifting_plugin: string
 end
 
 structure Lifting_BNF : LIFTING_BNF =
@@ -16,8 +15,6 @@
 open BNF_Def
 open Transfer_BNF
 
-val lifting_plugin = "lifting"
-
 (* Quotient map theorem *)
 
 fun Quotient_tac bnf ctxt i =
@@ -120,8 +117,10 @@
       lthy |> fold (perhaps o try o (snd oo Local_Theory.notes)) notess
     end
 
-val _ = Theory.setup (bnf_interpretation lifting_plugin
-  (bnf_only_type_ctr (BNF_Util.map_local_theory o lifting_bnf_interpretation))
-  (bnf_only_type_ctr lifting_bnf_interpretation))
+val lifting_plugin = Plugin_Name.declare_setup @{binding lifting}
+
+val _ =
+  Theory.setup
+    (bnf_interpretation lifting_plugin (bnf_only_type_ctr lifting_bnf_interpretation))
 
 end
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/Old_Datatype/old_datatype_data.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -237,28 +237,23 @@
 
 (** 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;
-
+val interpretation_data = Named_Target.theory_map o Old_Datatype_Plugin.data_default;
 
 
-(** setup theory **)
-
-val _ = Theory.setup Datatype_Interpretation.init;
-
 open Old_Datatype_Aux;
 
 end;
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -6,10 +6,6 @@
 
 signature EXHAUSTIVE_GENERATORS =
 sig
-  val exhaustive_plugin: string
-  val bounded_forall_plugin: string
-  val full_exhaustive_plugin: string
-
   val compile_generator_expr:
     Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
   val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
@@ -39,11 +35,6 @@
 
 (* basics *)
 
-val exhaustive_plugin = "quickcheck_exhaustive"
-val bounded_forall_plugin = "quickcheck_bounded_forall"
-val full_exhaustive_plugin = "quickcheck_full_exhaustive"
-
-
 (** dynamic options **)
 
 val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true)
@@ -544,11 +535,11 @@
 (* setup *)
 
 val setup_exhaustive_datatype_interpretation =
-  Quickcheck_Common.datatype_interpretation exhaustive_plugin
+  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_exhaustive}
     (@{sort exhaustive}, instantiate_exhaustive_datatype)
 
 val setup_bounded_forall_datatype_interpretation =
-  BNF_LFP_Compat.interpretation bounded_forall_plugin Quickcheck_Common.compat_prefs
+  BNF_LFP_Compat.interpretation @{plugin quickcheck_bounded_forall} Quickcheck_Common.compat_prefs
     (Quickcheck_Common.ensure_sort
        (((@{sort type}, @{sort type}), @{sort bounded_forall}),
        (fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs,
@@ -557,7 +548,7 @@
 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
 
 val setup =
-  Quickcheck_Common.datatype_interpretation full_exhaustive_plugin
+  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive}
     (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
   #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
   #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -6,7 +6,6 @@
 
 signature NARROWING_GENERATORS =
 sig
-  val narrowing_plugin: string
   val allow_existentials : bool Config.T
   val finite_functions : bool Config.T
   val overlord : bool Config.T
@@ -23,8 +22,6 @@
 structure Narrowing_Generators : NARROWING_GENERATORS =
 struct
 
-val narrowing_plugin = "quickcheck_narrowing"
-
 (* configurations *)
 
 val allow_existentials = Attrib.setup_config_bool @{binding quickcheck_allow_existentials} (K true)
@@ -528,7 +525,7 @@
 val setup =
   Code.datatype_interpretation ensure_partial_term_of
   #> Code.datatype_interpretation ensure_partial_term_of_code
-  #> Quickcheck_Common.datatype_interpretation narrowing_plugin
+  #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
     (@{sort narrowing}, instantiate_narrowing_datatype)
   #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
     
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -7,7 +7,6 @@
 signature RANDOM_GENERATORS =
 sig
   type seed = Random_Engine.seed
-  val random_plugin: string
   val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     -> seed -> (('a -> 'b) * (unit -> term)) * seed
@@ -25,8 +24,6 @@
 structure Random_Generators : RANDOM_GENERATORS =
 struct
 
-val random_plugin = "quickcheck_random";
-
 (** abstract syntax **)
 
 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
@@ -473,7 +470,7 @@
 val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
 
 val setup =
-  Quickcheck_Common.datatype_interpretation random_plugin
+  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_random}
     (@{sort random}, instantiate_random_datatype)
   #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
 
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -6,7 +6,6 @@
 
 signature TRANSFER_BNF =
 sig
-  val transfer_plugin: string
   val base_name_of_bnf: BNF_Def.bnf -> binding
   val type_name_of_bnf: BNF_Def.bnf -> string
   val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
@@ -21,8 +20,6 @@
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 
-val transfer_plugin = "transfer"
-
 (* util functions *)
 
 fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
@@ -282,6 +279,8 @@
 
 (* BNF interpretation *)
 
+val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}
+
 fun transfer_bnf_interpretation bnf lthy =
   let
     val dead = dead_of_bnf bnf
@@ -294,9 +293,9 @@
     |> predicator bnf
   end
 
-val _ = Theory.setup (bnf_interpretation transfer_plugin
-  (bnf_only_type_ctr (BNF_Util.map_local_theory o transfer_bnf_interpretation))
-  (bnf_only_type_ctr transfer_bnf_interpretation))
+val _ =
+  Theory.setup
+    (bnf_interpretation transfer_plugin (bnf_only_type_ctr transfer_bnf_interpretation))
 
 (* simplification rules for the predicator *)
 
@@ -370,8 +369,8 @@
     snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
   end
 
-val _ = Theory.setup (fp_sugars_interpretation transfer_plugin
-  (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugars_interpretation))
-  (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
+val _ =
+  Theory.setup (fp_sugars_interpretation transfer_plugin
+    (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
 
 end
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -7,15 +7,12 @@
 
 signature DATATYPE_REALIZER =
 sig
-  val extraction_plugin: string
   val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
 end;
 
 structure Datatype_Realizer : DATATYPE_REALIZER =
 struct
 
-val extraction_plugin = "extraction";
-
 fun subsets i j =
   if i <= j then
     let val is = subsets (i+1) j
@@ -241,6 +238,6 @@
       |> fold_rev (perhaps o try o make_casedists) infos
     end;
 
-val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin [] add_dt_realizers);
+val _ = Theory.setup (BNF_LFP_Compat.interpretation @{plugin extraction} [] add_dt_realizers);
 
 end;
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Tools/typedef.ML	Mon Oct 13 21:57:40 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 7f14d5d9b933 -r d2a7b443ceb2 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/HOL/Typerep.thy	Mon Oct 13 21:57:40 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)
 
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/Pure/Isar/code.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -1237,18 +1237,18 @@
 
 fun unoverload_const_typ thy (c, ty) = (Axclass.unoverload_const thy (c, ty), ty);
 
-structure Datatype_Interpretation =
-  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
+structure Datatype_Plugin = Plugin(type T = string);
+
+val datatype_plugin = Plugin_Name.declare_setup @{binding datatype_code};
 
-fun with_repaired_path f (tyco, serial) thy =
-  thy
-  |> Sign.root_path
-  |> Sign.add_path (Long_Name.qualifier tyco)
-  |> f (tyco, serial)
-  |> Sign.restore_naming thy;
-
-fun datatype_interpretation f = Datatype_Interpretation.interpretation
-  (fn (tyco, _) => fn thy => with_repaired_path f (tyco, fst (get_type thy tyco)) thy);
+fun datatype_interpretation f =
+  Datatype_Plugin.interpretation datatype_plugin
+    (fn tyco => Local_Theory.background_theory (fn thy =>
+      thy
+      |> Sign.root_path
+      |> Sign.add_path (Long_Name.qualifier tyco)
+      |> f (tyco, fst (get_type thy tyco))
+      |> Sign.restore_naming thy));
 
 fun add_datatype proto_constrs thy =
   let
@@ -1257,17 +1257,20 @@
   in
     thy
     |> register_type (tyco, (vs, Constructors (cos, [])))
-    |> Datatype_Interpretation.data (tyco, serial ())
+    |> Named_Target.theory_map (Datatype_Plugin.data_default tyco)
   end;
 
 fun add_datatype_cmd raw_constrs thy =
   add_datatype (map (read_bare_const thy) raw_constrs) thy;
 
-structure Abstype_Interpretation =
-  Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
+structure Abstype_Plugin = Plugin(type T = string);
+
+val abstype_plugin = Plugin_Name.declare_setup @{binding abstype_code};
 
-fun abstype_interpretation f = Abstype_Interpretation.interpretation
-  (fn (tyco, _) => fn thy => f (tyco, get_abstype_spec thy tyco) thy);
+fun abstype_interpretation f =
+  Abstype_Plugin.interpretation abstype_plugin
+    (fn tyco =>
+      Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy));
 
 fun add_abstype proto_thm thy =
   let
@@ -1278,7 +1281,7 @@
     |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
     |> change_fun_spec rep
       (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
-    |> Abstype_Interpretation.data (tyco, serial ())
+    |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
   end;
 
 
@@ -1299,8 +1302,7 @@
       || Args.$$$ "abort" -- Args.colon |-- (Scan.repeat1 Parse.term >> mk_const_attribute del_exception)
       || Scan.succeed (mk_attribute add_eqn_maybe_abs);
   in
-    Datatype_Interpretation.init
-    #> Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
+    Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
         "declare theorems for code generation"
   end);
 
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -13,6 +13,7 @@
   val class_of: local_theory -> string option
   val init: string -> theory -> local_theory
   val theory_init: theory -> local_theory
+  val theory_map: (local_theory -> local_theory) -> theory -> theory
   val theory_like_init: (local_theory -> local_theory) -> theory -> local_theory
   val begin: xstring * Position.T -> theory -> local_theory
   val exit: local_theory -> theory
@@ -176,6 +177,8 @@
 
 val theory_init = init "";
 
+fun theory_map f = theory_init #> f #> Local_Theory.exit_global;
+
 fun theory_like_init before_exit = gen_init (SOME before_exit) "";
 
 
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/Pure/Pure.thy
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/Pure/ROOT	Mon Oct 13 21:57:40 2014 +0200
@@ -210,6 +210,7 @@
     "Thy/thy_syntax.ML"
     "Tools/build.ML"
     "Tools/named_thms.ML"
+    "Tools/plugin.ML"
     "Tools/proof_general.ML"
     "assumption.ML"
     "axclass.ML"
@@ -227,7 +228,6 @@
     "global_theory.ML"
     "goal.ML"
     "goal_display.ML"
-    "interpretation.ML"
     "item_net.ML"
     "library.ML"
     "logic.ML"
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Oct 13 18:55:05 2014 +0200
+++ b/src/Pure/ROOT.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -181,7 +181,6 @@
 use "pattern.ML";
 use "unify.ML";
 use "theory.ML";
-use "interpretation.ML";
 use "proofterm.ML";
 use "thm.ML";
 use "more_thm.ML";
@@ -278,6 +277,7 @@
 use "Isar/bundle.ML";
 
 use "simplifier.ML";
+use "Tools/plugin.ML";
 
 (*executable theory content*)
 use "Isar/code.ML";
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/Pure/Tools/plugin.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 21:57:40 2014 +0200
@@ -0,0 +1,189 @@
+(*  Title:      Pure/Tools/plugin.ML
+    Author:     Makarius
+    Author:     Jasmin Blanchette
+
+Named plugins for definitional packages.
+*)
+
+(** plugin name **)
+
+signature PLUGIN_NAME =
+sig
+  val check: Proof.context -> xstring * Position.T -> string
+  val define: binding -> string list -> theory -> string * theory
+  val define_setup: binding -> string list -> string
+  val declare: binding -> theory -> string * theory
+  val declare_setup: binding -> string
+  type filter = string -> bool
+  val default_filter: filter
+  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
+  val parse_filter: (Proof.context -> filter) parser
+end;
+
+structure Plugin_Name: PLUGIN_NAME =
+struct
+
+(* theory data *)
+
+structure Data = Theory_Data
+(
+  type T = string list Name_Space.table;
+  val empty: T = Name_Space.empty_table "plugin";
+  val extend = I;
+  val merge = Name_Space.merge_tables;
+);
+
+
+(* check *)
+
+fun check ctxt =
+  #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt));
+
+val _ = Theory.setup
+  (ML_Antiquotation.inline @{binding plugin}
+    (Args.context -- Scan.lift (Parse.position Args.name)
+      >> (ML_Syntax.print_string o uncurry check)));
+
+
+(* indirections *)
+
+fun resolve thy = maps (fn name =>
+  (case Name_Space.get (Data.get thy) name of
+    [] => [name]
+  | names => resolve thy names));
+
+fun define binding rhs thy =
+  let
+    val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.default_naming);
+    val (name, data') = Name_Space.define context true (binding, resolve thy rhs) (Data.get thy);
+    val thy' = Data.put data' thy;
+  in (name, thy') end;
+
+fun define_setup binding rhs = Context.>>> (Context.map_theory_result (define binding rhs));
+
+
+(* immediate entries *)
+
+fun declare binding thy = define binding [] thy;
+fun declare_setup binding = Context.>>> (Context.map_theory_result (declare binding));
+
+
+(* filter *)
+
+type filter = string -> bool;
+
+val default_filter: filter = K true;
+
+fun make_filter (ctxt: Proof.context) f : filter = f ctxt;
+
+val parse_filter =
+  Parse.position (Parse.reserved "plugins") --
+    Parse.position (Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --
+    (Parse.$$$ ":" |-- Scan.repeat (Parse.position Parse.name)) >>
+      (fn (((_, pos1), (modif, pos2)), args) => fn ctxt =>
+        let
+          val thy = Proof_Context.theory_of ctxt;
+          val _ = Context_Position.reports ctxt (map (rpair Markup.quasi_keyword) [pos1, pos2]);
+          val basic_names = resolve thy (map (check ctxt) args);
+        in modif o member (op =) basic_names end);
+
+end;
+
+
+
+(** plugin content **)
+
+signature PLUGIN =
+sig
+  type T
+  val data: Plugin_Name.filter -> T -> local_theory -> local_theory
+  val data_default: T -> local_theory -> local_theory
+  val interpretation: string -> (T -> local_theory -> local_theory) -> theory -> theory
+end;
+
+functor Plugin(type T): PLUGIN =
+struct
+
+type T = T;
+
+
+(* data with interpretation *)
+
+type data = {filter: Plugin_Name.filter, naming: Name_Space.naming, value: T, id: serial};
+type interp = {name: string, apply: T -> local_theory -> local_theory, id: serial};
+
+val eq_data: data * data -> bool = op = o pairself #id;
+val eq_interp: interp * interp -> bool = op = o pairself #id;
+
+fun mk_data filter naming x : data = {filter = filter, naming = naming, value = x, id = serial ()};
+fun mk_interp name f : interp = {name = name, apply = f, id = serial ()};
+
+
+(* theory data *)
+
+structure Plugin_Data = Theory_Data
+(
+  type T = data list * (interp * data list) list;
+  val empty : T = ([], []);
+  val extend = I;
+  val merge_data = merge eq_data;
+  fun merge ((data1, interps1), (data2, interps2)) : T =
+    (merge_data (data1, data2), AList.join eq_interp (K merge_data) (interps1, interps2));
+);
+
+
+(* consolidate data wrt. interpretations *)
+
+local
+
+fun apply change_naming (interp: interp) (data: data) lthy =
+  lthy
+  |> change_naming ? Local_Theory.map_naming (K (#naming data))
+  |> #apply interp (#value data)
+  |> Local_Theory.restore_naming lthy;
+
+fun unfinished data (interp: interp, data') =
+  (interp,
+    if eq_list eq_data (data, data') then []
+    else data |> filter (fn d => #filter d (#name interp) andalso not (member eq_data data' d)));
+
+fun unfinished_data thy =
+  let
+    val (data, interps) = Plugin_Data.get thy;
+    val finished = map (apsnd (K data)) interps;
+    val thy' = Plugin_Data.put (data, finished) thy;
+  in (map (unfinished data) interps, thy') end;
+
+in
+
+val consolidate =
+  Local_Theory.raw_theory_result unfinished_data
+  #-> fold_rev (fn (interp, data) => fold_rev (apply false interp) data);
+
+val consolidate' =
+  unfinished_data #> (fn (unfinished, thy) =>
+    if forall (null o #2) unfinished then NONE
+    else
+      SOME (Named_Target.theory_map
+        (fold_rev (fn (interp, data) => fold_rev (apply true interp) data) unfinished) thy));
+
+end;
+
+val _ = Theory.setup (Theory.at_begin consolidate');
+
+
+(* add content *)
+
+fun data filter x =
+  Local_Theory.background_theory (fn thy =>
+    Plugin_Data.map (apfst (cons (mk_data filter (Sign.naming_of thy) x))) thy)
+  #> consolidate;
+
+val data_default = data Plugin_Name.default_filter;
+
+fun interpretation name f =
+  Plugin_Data.map (apsnd (cons (mk_interp name f, [])))
+  #> perhaps consolidate';
+
+end;
+
diff -r 7f14d5d9b933 -r d2a7b443ceb2 src/Pure/interpretation.ML
--- a/src/Pure/interpretation.ML	Mon Oct 13 18:55:05 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(*  Title:      Pure/interpretation.ML
-    Author:     Florian Haftmann and Makarius
-
-Generic interpretation of theory data.
-*)
-
-signature INTERPRETATION =
-sig
-  type T
-  val result: theory -> T list
-  val interpretation: (T -> theory -> theory) -> theory -> theory
-  val data: T -> theory -> theory
-  val init: theory -> theory
-end;
-
-functor Interpretation(type T val eq: T * T -> bool): INTERPRETATION =
-struct
-
-type T = T;
-
-structure Interp = Theory_Data
-(
-  type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
-  val empty = ([], []);
-  val extend = I;
-  fun merge ((data1, interps1), (data2, interps2)) : T =
-    (Library.merge eq (data1, data2),
-     AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
-);
-
-val result = #1 o Interp.get;
-
-fun consolidate thy =
-  let
-    val (data, interps) = Interp.get thy;
-    val unfinished = interps |> map (fn ((f, _), xs) =>
-      (f, if eq_list eq (xs, data) then [] else subtract eq xs data));
-    val finished = interps |> map (fn (interp, _) => (interp, data));
-  in
-    if forall (null o #2) unfinished then NONE
-    else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))
-  end;
-
-fun interpretation f = Interp.map (apsnd (cons ((f, stamp ()), []))) #> perhaps consolidate;
-fun data x = Interp.map (apfst (cons x)) #> perhaps consolidate;
-
-val init = Theory.at_begin consolidate;
-
-end;