Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
authorwenzelm
Mon Oct 13 18:45:48 2014 +0200 (2014-10-13)
changeset 586596c9821c32dd5
parent 58658 9002fe021e2f
child 58660 8d4aebb9e327
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
src/Doc/Datatypes/Datatypes.thy
src/HOL/Ctr_Sugar.thy
src/HOL/Enum.thy
src/HOL/HOL.thy
src/HOL/Library/bnf_axiomatization.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
src/HOL/Tools/Ctr_Sugar/local_interpretation.ML
src/HOL/Tools/Lifting/lifting_bnf.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
src/HOL/Tools/datatype_realizer.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Oct 13 17:04:25 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Oct 13 18:45:48 2014 +0200
     1.3 @@ -500,8 +500,10 @@
     1.4  
     1.5  \item
     1.6  The @{text "plugins"} option indicates which plugins should be enabled
     1.7 -(@{text only}) or disabled (@{text del}). Wildcards (``@{text "*"}'') are
     1.8 -allowed (e.g., @{text "quickcheck_*"}). By default, all plugins are enabled.
     1.9 +(@{text only}) or disabled (@{text del}). Some plugin names are defined
    1.10 +as indirection to a group of sub-plugins (notably @{text "quickcheck"}
    1.11 +based on @{text quickcheck_random}, @{text quickcheck_exhaustive}, \dots).
    1.12 +By default, all plugins are enabled.
    1.13  
    1.14  \item
    1.15  The @{text "discs_sels"} option indicates that discriminators and selectors
    1.16 @@ -2794,7 +2796,7 @@
    1.17  For example:
    1.18  *}
    1.19  
    1.20 -    datatype (plugins del: code "quickcheck_*") color = Red | Black
    1.21 +    datatype (plugins del: code "quickcheck") color = Red | Black
    1.22  
    1.23  
    1.24  subsection {* Code Generator
     2.1 --- a/src/HOL/Ctr_Sugar.thy	Mon Oct 13 17:04:25 2014 +0200
     2.2 +++ b/src/HOL/Ctr_Sugar.thy	Mon Oct 13 18:45:48 2014 +0200
     2.3 @@ -37,7 +37,6 @@
     2.4    "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
     2.5    by blast+
     2.6  
     2.7 -ML_file "Tools/Ctr_Sugar/local_interpretation.ML"
     2.8  ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
     2.9  ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
    2.10  ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
     3.1 --- a/src/HOL/Enum.thy	Mon Oct 13 17:04:25 2014 +0200
     3.2 +++ b/src/HOL/Enum.thy	Mon Oct 13 18:45:48 2014 +0200
     3.3 @@ -493,7 +493,7 @@
     3.4  
     3.5  text {* We define small finite types for use in Quickcheck *}
     3.6  
     3.7 -datatype (plugins only: code "quickcheck*" extraction) finite_1 =
     3.8 +datatype (plugins only: code "quickcheck" extraction) finite_1 =
     3.9    a\<^sub>1
    3.10  
    3.11  notation (output) a\<^sub>1  ("a\<^sub>1")
    3.12 @@ -596,7 +596,7 @@
    3.13  declare [[simproc del: finite_1_eq]]
    3.14  hide_const (open) a\<^sub>1
    3.15  
    3.16 -datatype (plugins only: code "quickcheck*" extraction) finite_2 =
    3.17 +datatype (plugins only: code "quickcheck" extraction) finite_2 =
    3.18    a\<^sub>1 | a\<^sub>2
    3.19  
    3.20  notation (output) a\<^sub>1  ("a\<^sub>1")
    3.21 @@ -711,7 +711,7 @@
    3.22  
    3.23  hide_const (open) a\<^sub>1 a\<^sub>2
    3.24  
    3.25 -datatype (plugins only: code "quickcheck*" extraction) finite_3 =
    3.26 +datatype (plugins only: code "quickcheck" extraction) finite_3 =
    3.27    a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    3.28  
    3.29  notation (output) a\<^sub>1  ("a\<^sub>1")
    3.30 @@ -838,7 +838,7 @@
    3.31  
    3.32  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
    3.33  
    3.34 -datatype (plugins only: code "quickcheck*" extraction) finite_4 =
    3.35 +datatype (plugins only: code "quickcheck" extraction) finite_4 =
    3.36    a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    3.37  
    3.38  notation (output) a\<^sub>1  ("a\<^sub>1")
    3.39 @@ -940,7 +940,7 @@
    3.40  
    3.41  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
    3.42  
    3.43 -datatype (plugins only: code "quickcheck*" extraction) finite_5 =
    3.44 +datatype (plugins only: code "quickcheck" extraction) finite_5 =
    3.45    a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    3.46  
    3.47  notation (output) a\<^sub>1  ("a\<^sub>1")
     4.1 --- a/src/HOL/HOL.thy	Mon Oct 13 17:04:25 2014 +0200
     4.2 +++ b/src/HOL/HOL.thy	Mon Oct 13 18:45:48 2014 +0200
     4.3 @@ -40,6 +40,25 @@
     4.4    #> Case_Product.setup
     4.5  *}
     4.6  
     4.7 +ML \<open>Plugin_Name.declare_setup @{binding extraction}\<close>
     4.8 +
     4.9 +ML \<open>
    4.10 +  Plugin_Name.declare_setup @{binding quickcheck_random};
    4.11 +  Plugin_Name.declare_setup @{binding quickcheck_exhaustive};
    4.12 +  Plugin_Name.declare_setup @{binding quickcheck_bounded_forall};
    4.13 +  Plugin_Name.declare_setup @{binding quickcheck_full_exhaustive};
    4.14 +  Plugin_Name.declare_setup @{binding quickcheck_narrowing};
    4.15 +\<close>
    4.16 +ML \<open>
    4.17 +  Plugin_Name.define_setup @{binding quickcheck}
    4.18 +   [@{plugin quickcheck_exhaustive},
    4.19 +    @{plugin quickcheck_random},
    4.20 +    @{plugin quickcheck_bounded_forall},
    4.21 +    @{plugin quickcheck_full_exhaustive},
    4.22 +    @{plugin quickcheck_narrowing}]
    4.23 +\<close>
    4.24 +
    4.25 +
    4.26  subsection {* Primitive logic *}
    4.27  
    4.28  subsubsection {* Core syntax *}
     5.1 --- a/src/HOL/Library/bnf_axiomatization.ML	Mon Oct 13 17:04:25 2014 +0200
     5.2 +++ b/src/HOL/Library/bnf_axiomatization.ML	Mon Oct 13 18:45:48 2014 +0200
     5.3 @@ -17,9 +17,11 @@
     5.4  open BNF_Util
     5.5  open BNF_Def
     5.6  
     5.7 -fun prepare_decl prepare_constraint prepare_typ plugins raw_vars b mx user_mapb user_relb user_witTs
     5.8 -  lthy =
     5.9 +fun prepare_decl prepare_plugins prepare_constraint prepare_typ
    5.10 +    raw_plugins raw_vars b mx user_mapb user_relb user_witTs lthy =
    5.11    let
    5.12 +   val plugins = prepare_plugins lthy raw_plugins;
    5.13 +
    5.14     fun prepare_type_arg (set_opt, (ty, c)) =
    5.15        let val s = fst (dest_TFree (prepare_typ lthy ty)) in
    5.16          (set_opt, (s, prepare_constraint lthy c))
    5.17 @@ -95,12 +97,12 @@
    5.18      (bnf, register_bnf plugins key bnf lthy')
    5.19    end;
    5.20  
    5.21 -val bnf_axiomatization = prepare_decl (K I) (K I);
    5.22 +val bnf_axiomatization = prepare_decl (K I) (K I) (K I);
    5.23  
    5.24  fun read_constraint _ NONE = @{sort type}
    5.25    | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
    5.26  
    5.27 -val bnf_axiomatization_cmd = prepare_decl read_constraint Syntax.read_typ;
    5.28 +val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ;
    5.29  
    5.30  val parse_witTs =
    5.31    @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
    5.32 @@ -109,7 +111,7 @@
    5.33    @{keyword "]"} || Scan.succeed [];
    5.34  
    5.35  val parse_bnf_axiomatization_options =
    5.36 -  Scan.optional (@{keyword "("} |-- parse_plugins --| @{keyword ")"}) (K true);
    5.37 +  Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"}) (K (K true));
    5.38  
    5.39  val parse_bnf_axiomatization =
    5.40    parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding --
     6.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Oct 13 17:04:25 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Oct 13 18:45:48 2014 +0200
     6.3 @@ -17,8 +17,7 @@
     6.4    val transfer_bnf: theory -> bnf -> bnf
     6.5    val bnf_of: Proof.context -> string -> bnf option
     6.6    val bnf_of_global: theory -> string -> bnf option
     6.7 -  val bnf_interpretation: string -> (bnf -> theory -> theory) ->
     6.8 -    (bnf -> local_theory -> local_theory) -> theory -> theory
     6.9 +  val bnf_interpretation: string -> (bnf -> local_theory -> local_theory) -> theory -> theory
    6.10    val interpret_bnf: (string -> bool) -> bnf -> local_theory -> local_theory
    6.11    val register_bnf_raw: string -> bnf -> local_theory -> local_theory
    6.12    val register_bnf: (string -> bool) -> string -> bnf -> local_theory -> local_theory
    6.13 @@ -1514,18 +1513,13 @@
    6.14      (key, goals, wit_goalss, after_qed, lthy, one_step_defs)
    6.15    end;
    6.16  
    6.17 -structure BNF_Interpretation = Local_Interpretation
    6.18 -(
    6.19 -  type T = bnf;
    6.20 -  val eq: T * T -> bool = op = o pairself T_of_bnf;
    6.21 -);
    6.22 +structure BNF_Plugin = Plugin(type T = bnf);
    6.23  
    6.24 -fun with_transfer_bnf g bnf thy = g (transfer_bnf thy bnf) thy;
    6.25 +fun bnf_interpretation name f =
    6.26 +  BNF_Plugin.interpretation name
    6.27 +    (fn bnf => fn lthy => f (transfer_bnf (Proof_Context.theory_of lthy) bnf) lthy);
    6.28  
    6.29 -fun bnf_interpretation name =
    6.30 -  BNF_Interpretation.interpretation name o with_transfer_bnf;
    6.31 -
    6.32 -val interpret_bnf = BNF_Interpretation.data;
    6.33 +val interpret_bnf = BNF_Plugin.data;
    6.34  
    6.35  fun register_bnf_raw key bnf =
    6.36    Local_Theory.declaration {syntax = false, pervasive = true}
    6.37 @@ -1557,9 +1551,10 @@
    6.38    end) o prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs
    6.39      raw_csts;
    6.40  
    6.41 -fun bnf_cmd (raw_csts, plugins) =
    6.42 +fun bnf_cmd (raw_csts, raw_plugins) =
    6.43    (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
    6.44    let
    6.45 +    val plugins = raw_plugins lthy;
    6.46      val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
    6.47      fun mk_triv_wit_thms tac set_maps =
    6.48        Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
    6.49 @@ -1619,9 +1614,7 @@
    6.50           Scan.repeat1 (Scan.unless (Parse.reserved "rel" ||
    6.51             Parse.reserved "plugins") Parse.term)) [] --
    6.52         Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) --
    6.53 -       Scan.optional parse_plugins (K true)
    6.54 +       Scan.optional Plugin_Name.parse_filter (K (K true))
    6.55         >> bnf_cmd);
    6.56  
    6.57 -val _ = Context.>> (Context.map_theory BNF_Interpretation.init);
    6.58 -
    6.59  end;
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 13 17:04:25 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 13 18:45:48 2014 +0200
     7.3 @@ -67,7 +67,7 @@
     7.4    val fp_sugar_of_global: theory -> string -> fp_sugar option
     7.5    val fp_sugars_of: Proof.context -> fp_sugar list
     7.6    val fp_sugars_of_global: theory -> fp_sugar list
     7.7 -  val fp_sugars_interpretation: string -> (fp_sugar list -> theory -> theory) ->
     7.8 +  val fp_sugars_interpretation: string ->
     7.9      (fp_sugar list -> local_theory -> local_theory)-> theory -> theory
    7.10    val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
    7.11    val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
    7.12 @@ -316,18 +316,14 @@
    7.13  fun co_induct_of (i :: _) = i;
    7.14  fun strong_co_induct_of [_, s] = s;
    7.15  
    7.16 -structure FP_Sugar_Interpretation = Local_Interpretation
    7.17 -(
    7.18 -  type T = fp_sugar list;
    7.19 -  val eq: T * T -> bool = op = o pairself (map #T);
    7.20 -);
    7.21 +structure FP_Sugar_Plugin = Plugin(type T = fp_sugar list);
    7.22  
    7.23 -fun with_transfer_fp_sugars g fp_sugars thy = g (map (transfer_fp_sugar thy) fp_sugars) thy;
    7.24 +fun fp_sugars_interpretation name f =
    7.25 +  FP_Sugar_Plugin.interpretation name
    7.26 +    (fn fp_sugars => fn lthy =>
    7.27 +      f (map (transfer_fp_sugar (Proof_Context.theory_of lthy)) fp_sugars) lthy);
    7.28  
    7.29 -fun fp_sugars_interpretation name =
    7.30 -  FP_Sugar_Interpretation.interpretation name o with_transfer_fp_sugars;
    7.31 -
    7.32 -val interpret_fp_sugars = FP_Sugar_Interpretation.data;
    7.33 +val interpret_fp_sugars = FP_Sugar_Plugin.data;
    7.34  
    7.35  fun register_fp_sugars_raw fp_sugars =
    7.36    fold (fn fp_sugar as {T = Type (s, _), ...} =>
    7.37 @@ -984,7 +980,7 @@
    7.38              |> map Thm.close_derivation
    7.39          end;
    7.40  
    7.41 -      val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
    7.42 +      val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
    7.43  
    7.44        val anonymous_notes =
    7.45          [(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
    7.46 @@ -1417,7 +1413,7 @@
    7.47  
    7.48      val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
    7.49  
    7.50 -    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
    7.51 +    val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
    7.52    in
    7.53      ((induct_thms, induct_thm, mk_induct_attrs ctrss),
    7.54       (rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs))
    7.55 @@ -1828,11 +1824,12 @@
    7.56       (corec_sel_thmsss, simp_attrs))
    7.57    end;
    7.58  
    7.59 -fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
    7.60 -    ((plugins, discs_sels0), specs) no_defs_lthy =
    7.61 +fun define_co_datatypes prepare_plugins prepare_constraint prepare_typ prepare_term fp construct_fp
    7.62 +    ((raw_plugins, discs_sels0), specs) no_defs_lthy =
    7.63    let
    7.64      (* TODO: sanity checks on arguments *)
    7.65  
    7.66 +    val plugins = prepare_plugins no_defs_lthy raw_plugins;
    7.67      val discs_sels = discs_sels0 orelse fp = Greatest_FP;
    7.68  
    7.69      val nn = length specs;
    7.70 @@ -2010,7 +2007,7 @@
    7.71      val fpTs = map (domain_type o fastype_of) dtors;
    7.72      val fpBTs = map B_ify_T fpTs;
    7.73  
    7.74 -    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
    7.75 +    val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
    7.76  
    7.77      val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
    7.78      val ns = map length ctr_Tsss;
    7.79 @@ -2375,10 +2372,11 @@
    7.80      timer; lthy''
    7.81    end;
    7.82  
    7.83 -fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) x;
    7.84 +fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) (K I) x;
    7.85  
    7.86  fun co_datatype_cmd x =
    7.87 -  define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x;
    7.88 +  define_co_datatypes Plugin_Name.make_filter Typedecl.read_constraint
    7.89 +    Syntax.parse_typ Syntax.parse_term x;
    7.90  
    7.91  val parse_ctr_arg =
    7.92    @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"}
    7.93 @@ -2395,6 +2393,4 @@
    7.94  
    7.95  fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
    7.96  
    7.97 -val _ = Theory.setup FP_Sugar_Interpretation.init;
    7.98 -
    7.99  end;
     8.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Oct 13 17:04:25 2014 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Oct 13 18:45:48 2014 +0200
     8.3 @@ -451,10 +451,8 @@
     8.4    end;
     8.5  
     8.6  fun interpretation name prefs f =
     8.7 -  let val new_f = new_interpretation_of prefs f in
     8.8 -    Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
     8.9 -    #> fp_sugars_interpretation name new_f (Local_Theory.background_theory o new_f)
    8.10 -  end;
    8.11 +  Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
    8.12 +  #> fp_sugars_interpretation name (Local_Theory.background_theory o new_interpretation_of prefs f);
    8.13  
    8.14  val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
    8.15  
     9.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Oct 13 17:04:25 2014 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Oct 13 18:45:48 2014 +0200
     9.3 @@ -7,7 +7,6 @@
     9.4  
     9.5  signature BNF_LFP_SIZE =
     9.6  sig
     9.7 -  val size_plugin: string
     9.8    val register_size: string -> string -> thm list -> thm list -> local_theory -> local_theory
     9.9    val register_size_global: string -> string -> thm list -> thm list -> theory -> theory
    9.10    val size_of: Proof.context -> string -> (string * (thm list * thm list)) option
    9.11 @@ -22,8 +21,6 @@
    9.12  open BNF_Def
    9.13  open BNF_FP_Def_Sugar
    9.14  
    9.15 -val size_plugin = "size";
    9.16 -
    9.17  val size_N = "size_";
    9.18  
    9.19  val rec_o_mapN = "rec_o_map";
    9.20 @@ -396,7 +393,7 @@
    9.21      end
    9.22    | generate_datatype_size _ lthy = lthy;
    9.23  
    9.24 -val _ = Theory.setup (fp_sugars_interpretation size_plugin
    9.25 -  (map_local_theory o generate_datatype_size) generate_datatype_size);
    9.26 +val size_plugin = Plugin_Name.declare_setup @{binding size};
    9.27 +val _ = Theory.setup (fp_sugars_interpretation size_plugin generate_datatype_size);
    9.28  
    9.29  end;
    10.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Oct 13 17:04:25 2014 +0200
    10.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Oct 13 18:45:48 2014 +0200
    10.3 @@ -7,8 +7,6 @@
    10.4  
    10.5  signature CTR_SUGAR =
    10.6  sig
    10.7 -  val code_plugin: string
    10.8 -
    10.9    type ctr_sugar =
   10.10      {T: typ,
   10.11       ctrs: term list,
   10.12 @@ -46,7 +44,7 @@
   10.13    val ctr_sugars_of_global: theory -> ctr_sugar list
   10.14    val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
   10.15    val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
   10.16 -  val ctr_sugar_interpretation: string -> (ctr_sugar -> theory -> theory) ->
   10.17 +  val ctr_sugar_interpretation: string ->
   10.18      (ctr_sugar -> local_theory -> local_theory) -> theory -> theory
   10.19    val interpret_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
   10.20    val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory
   10.21 @@ -72,14 +70,16 @@
   10.22    val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
   10.23  
   10.24    type ctr_options = (string -> bool) * bool
   10.25 +  type ctr_options_cmd = (Proof.context -> string -> bool) * bool
   10.26  
   10.27    val fake_local_theory_for_sel_defaults: (binding * typ) list -> Proof.context -> Proof.context
   10.28    val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
   10.29      ((ctr_options * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
   10.30      ctr_sugar * local_theory
   10.31    val default_ctr_options: ctr_options
   10.32 +  val default_ctr_options_cmd: ctr_options_cmd
   10.33    val parse_bound_term: (binding * string) parser
   10.34 -  val parse_ctr_options: ctr_options parser
   10.35 +  val parse_ctr_options: ctr_options_cmd parser
   10.36    val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a) ctr_spec parser
   10.37    val parse_sel_default_eqs: string list parser
   10.38  end;
   10.39 @@ -91,8 +91,6 @@
   10.40  open Ctr_Sugar_Tactics
   10.41  open Ctr_Sugar_Code
   10.42  
   10.43 -val code_plugin = "code";
   10.44 -
   10.45  type ctr_sugar =
   10.46    {T: typ,
   10.47     ctrs: term list,
   10.48 @@ -183,18 +181,14 @@
   10.49  val ctr_sugar_of_case = ctr_sugar_of_case_generic o Context.Proof;
   10.50  val ctr_sugar_of_case_global = ctr_sugar_of_case_generic o Context.Theory;
   10.51  
   10.52 -structure Ctr_Sugar_Interpretation = Local_Interpretation
   10.53 -(
   10.54 -  type T = ctr_sugar;
   10.55 -  val eq: T * T -> bool = op = o pairself #ctrs;
   10.56 -);
   10.57 +structure Ctr_Sugar_Plugin = Plugin(type T = ctr_sugar);
   10.58  
   10.59 -fun with_transfer_ctr_sugar g ctr_sugar thy = g (transfer_ctr_sugar thy ctr_sugar) thy;
   10.60 +fun ctr_sugar_interpretation name f =
   10.61 +  Ctr_Sugar_Plugin.interpretation name
   10.62 +    (fn ctr_sugar => fn lthy =>
   10.63 +      f (transfer_ctr_sugar (Proof_Context.theory_of lthy) ctr_sugar) lthy);
   10.64  
   10.65 -fun ctr_sugar_interpretation name =
   10.66 -  Ctr_Sugar_Interpretation.interpretation name o with_transfer_ctr_sugar;
   10.67 -
   10.68 -val interpret_ctr_sugar = Ctr_Sugar_Interpretation.data;
   10.69 +val interpret_ctr_sugar = Ctr_Sugar_Plugin.data;
   10.70  
   10.71  fun register_ctr_sugar_raw (ctr_sugar as {T = Type (s, _), ...}) =
   10.72    Local_Theory.declaration {syntax = false, pervasive = true}
   10.73 @@ -210,7 +204,9 @@
   10.74      else
   10.75        thy
   10.76        |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
   10.77 -      |> Ctr_Sugar_Interpretation.data_global plugins ctr_sugar
   10.78 +      |> Named_Target.theory_init
   10.79 +      |> Ctr_Sugar_Plugin.data plugins ctr_sugar
   10.80 +      |> Local_Theory.exit_global
   10.81    end;
   10.82  
   10.83  val isN = "is_";
   10.84 @@ -364,9 +360,15 @@
   10.85  fun ctr_of_ctr_spec ((_, ctr), _) = ctr;
   10.86  fun args_of_ctr_spec (_, args) = args;
   10.87  
   10.88 -fun prepare_free_constructors prep_term ((((plugins, discs_sels), raw_case_binding), ctr_specs),
   10.89 -    sel_default_eqs) no_defs_lthy =
   10.90 +val code_plugin = Plugin_Name.declare_setup @{binding code};
   10.91 +
   10.92 +fun prepare_free_constructors prep_plugins prep_term
   10.93 +    ((((raw_plugins, discs_sels), raw_case_binding), ctr_specs),
   10.94 +      sel_default_eqs) no_defs_lthy =
   10.95    let
   10.96 +    val plugins = prep_plugins no_defs_lthy raw_plugins;
   10.97 +
   10.98 +
   10.99      (* TODO: sanity checks on arguments *)
  10.100  
  10.101      val raw_ctrs = map ctr_of_ctr_spec ctr_specs;
  10.102 @@ -1056,24 +1058,27 @@
  10.103  
  10.104  fun free_constructors tacss = (fn (goalss, after_qed, lthy) =>
  10.105    map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
  10.106 -  |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I);
  10.107 +  |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I) (K I);
  10.108  
  10.109  val free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
  10.110    Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
  10.111 -  prepare_free_constructors Syntax.read_term;
  10.112 +  prepare_free_constructors Plugin_Name.make_filter Syntax.read_term;
  10.113  
  10.114  val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
  10.115  
  10.116  type ctr_options = (string -> bool) * bool;
  10.117 +type ctr_options_cmd = (Proof.context -> string -> bool) * bool;
  10.118  
  10.119 -val default_ctr_options = (K true, false) : ctr_options;
  10.120 +val default_ctr_options : ctr_options = (K true, false);
  10.121 +val default_ctr_options_cmd : ctr_options_cmd = (K (K true), false);
  10.122  
  10.123  val parse_ctr_options =
  10.124    Scan.optional (@{keyword "("} |-- Parse.list1
  10.125 -        (parse_plugins >> (apfst o K) || Parse.reserved "discs_sels" >> (apsnd o K o K true)) --|
  10.126 +        (Plugin_Name.parse_filter >> (apfst o K) ||
  10.127 +         Parse.reserved "discs_sels" >> (apsnd o K o K true)) --|
  10.128        @{keyword ")"}
  10.129 -      >> (fn fs => fold I fs default_ctr_options))
  10.130 -    default_ctr_options;
  10.131 +      >> (fn fs => fold I fs default_ctr_options_cmd))
  10.132 +    default_ctr_options_cmd;
  10.133  
  10.134  fun parse_ctr_spec parse_ctr parse_arg =
  10.135    parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg;
  10.136 @@ -1088,6 +1093,4 @@
  10.137         -- parse_sel_default_eqs
  10.138       >> free_constructors_cmd);
  10.139  
  10.140 -val _ = Theory.setup Ctr_Sugar_Interpretation.init;
  10.141 -
  10.142  end;
    11.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Oct 13 17:04:25 2014 +0200
    11.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Mon Oct 13 18:45:48 2014 +0200
    11.3 @@ -71,7 +71,6 @@
    11.4    val standard_binding: binding
    11.5    val parse_binding_colon: binding parser
    11.6    val parse_opt_binding_colon: binding parser
    11.7 -  val parse_plugins: (string -> bool) parser
    11.8  
    11.9    val ss_only: thm list -> Proof.context -> Proof.context
   11.10  
   11.11 @@ -87,18 +86,6 @@
   11.12  structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
   11.13  struct
   11.14  
   11.15 -fun match_entire_string pat s =
   11.16 -  let
   11.17 -    fun match [] [] = true
   11.18 -      | match [] _ = false
   11.19 -      | match (ps as #"*" :: ps') cs =
   11.20 -        match ps' cs orelse (not (null cs) andalso match ps (tl cs))
   11.21 -      | match _ [] = false
   11.22 -      | match (p :: ps) (c :: cs) = p = c andalso match ps cs;
   11.23 -  in
   11.24 -    match (String.explode pat) (String.explode s)
   11.25 -  end;
   11.26 -
   11.27  fun map_prod f g (x, y) = (f x, g y);
   11.28  
   11.29  fun seq_conds f n k xs =
   11.30 @@ -262,12 +249,6 @@
   11.31  val parse_binding_colon = Parse.binding --| @{keyword ":"};
   11.32  val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
   11.33  
   11.34 -val parse_plugins =
   11.35 -  Parse.reserved "plugins" |--
   11.36 -    ((Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --| @{keyword ":"}
   11.37 -     -- Scan.repeat (Parse.short_ident || Parse.string))
   11.38 -  >> (fn (modif, pats) => modif o member (uncurry match_entire_string o swap) pats);
   11.39 -
   11.40  fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
   11.41  
   11.42  (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
    12.1 --- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Mon Oct 13 17:04:25 2014 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,85 +0,0 @@
    12.4 -(*  Title:      HOL/Tools/Ctr_Sugar/local_interpretation.ML
    12.5 -    Author:     Jasmin Blanchette, TU Muenchen
    12.6 -
    12.7 -Generic interpretation of local theory data -- ad hoc. Based on
    12.8 -
    12.9 -    Title:      Pure/interpretation.ML
   12.10 -    Author:     Florian Haftmann and Makarius
   12.11 -*)
   12.12 -
   12.13 -signature LOCAL_INTERPRETATION =
   12.14 -sig
   12.15 -  type T
   12.16 -  val result: theory -> T list
   12.17 -  val interpretation: string -> (T -> theory -> theory) -> (T -> local_theory -> local_theory) ->
   12.18 -    theory -> theory
   12.19 -  val data: (string -> bool) -> T -> local_theory -> local_theory
   12.20 -  val data_global: (string -> bool) -> T -> theory -> theory
   12.21 -  val init: theory -> theory
   12.22 -end;
   12.23 -
   12.24 -functor Local_Interpretation(type T val eq: T * T -> bool): LOCAL_INTERPRETATION =
   12.25 -struct
   12.26 -
   12.27 -type T = T;
   12.28 -
   12.29 -structure Interp = Theory_Data
   12.30 -(
   12.31 -  type T =
   12.32 -    ((Name_Space.naming * (string -> bool)) * T) list
   12.33 -    * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * (string * stamp))
   12.34 -       * ((Name_Space.naming * (string -> bool)) * T) list) list;
   12.35 -  val empty = ([], []);
   12.36 -  val extend = I;
   12.37 -  fun merge ((data1, interps1), (data2, interps2)) : T =
   12.38 -    (Library.merge (eq_snd eq) (data1, data2),
   12.39 -     AList.join (eq_snd (op =)) (K (Library.merge (eq_snd eq))) (interps1, interps2));
   12.40 -);
   12.41 -
   12.42 -val result = map snd o fst o Interp.get;
   12.43 -
   12.44 -fun consolidate_common g_or_f lift_lthy thy thy_or_lthy =
   12.45 -  let
   12.46 -    val (data, interps) = Interp.get thy;
   12.47 -
   12.48 -    fun unfinished_of ((gf, (name, _)), data') =
   12.49 -      (g_or_f gf,
   12.50 -       if eq_list (eq_snd eq) (data', data) then
   12.51 -         []
   12.52 -       else
   12.53 -         subtract (eq_snd eq) data' data
   12.54 -         |> map_filter (fn ((naming, keep), x) => if keep name then SOME (naming, x) else NONE));
   12.55 -
   12.56 -    val unfinished = map unfinished_of interps;
   12.57 -    val finished = map (apsnd (K data)) interps;
   12.58 -  in
   12.59 -    if forall (null o #2) unfinished then
   12.60 -      NONE
   12.61 -    else
   12.62 -      SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
   12.63 -        |> lift_lthy (Interp.put (data, finished)))
   12.64 -  end;
   12.65 -
   12.66 -fun consolidate lthy =
   12.67 -  consolidate_common (fn (_, g) => fn (_, x) => g x) Local_Theory.background_theory
   12.68 -    (Proof_Context.theory_of lthy) lthy;
   12.69 -
   12.70 -fun consolidate_global thy =
   12.71 -  consolidate_common (fn (f, _) => fn (naming, x) => fn thy =>
   12.72 -    thy |> Sign.map_naming (K naming) |> f x |> Sign.restore_naming thy) I thy thy;
   12.73 -
   12.74 -fun interpretation name g f =
   12.75 -  Interp.map (apsnd (cons (((g, f), (name, stamp ())), []))) #> perhaps consolidate_global;
   12.76 -
   12.77 -fun data keep x =
   12.78 -  Local_Theory.background_theory
   12.79 -    (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
   12.80 -  #> perhaps consolidate;
   12.81 -
   12.82 -fun data_global keep x =
   12.83 -  (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
   12.84 -  #> perhaps consolidate_global;
   12.85 -
   12.86 -val init = Theory.at_begin consolidate_global;
   12.87 -
   12.88 -end;
    13.1 --- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Oct 13 17:04:25 2014 +0200
    13.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Oct 13 18:45:48 2014 +0200
    13.3 @@ -6,7 +6,6 @@
    13.4  
    13.5  signature LIFTING_BNF =
    13.6  sig
    13.7 -  val lifting_plugin: string
    13.8  end
    13.9  
   13.10  structure Lifting_BNF : LIFTING_BNF =
   13.11 @@ -16,8 +15,6 @@
   13.12  open BNF_Def
   13.13  open Transfer_BNF
   13.14  
   13.15 -val lifting_plugin = "lifting"
   13.16 -
   13.17  (* Quotient map theorem *)
   13.18  
   13.19  fun Quotient_tac bnf ctxt i =
   13.20 @@ -120,8 +117,10 @@
   13.21        lthy |> fold (perhaps o try o (snd oo Local_Theory.notes)) notess
   13.22      end
   13.23  
   13.24 -val _ = Theory.setup (bnf_interpretation lifting_plugin
   13.25 -  (bnf_only_type_ctr (BNF_Util.map_local_theory o lifting_bnf_interpretation))
   13.26 -  (bnf_only_type_ctr lifting_bnf_interpretation))
   13.27 +val lifting_plugin = Plugin_Name.declare_setup @{binding lifting}
   13.28 +
   13.29 +val _ =
   13.30 +  Theory.setup
   13.31 +    (bnf_interpretation lifting_plugin (bnf_only_type_ctr lifting_bnf_interpretation))
   13.32  
   13.33  end
    14.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Oct 13 17:04:25 2014 +0200
    14.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Oct 13 18:45:48 2014 +0200
    14.3 @@ -6,10 +6,6 @@
    14.4  
    14.5  signature EXHAUSTIVE_GENERATORS =
    14.6  sig
    14.7 -  val exhaustive_plugin: string
    14.8 -  val bounded_forall_plugin: string
    14.9 -  val full_exhaustive_plugin: string
   14.10 -
   14.11    val compile_generator_expr:
   14.12      Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
   14.13    val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
   14.14 @@ -39,11 +35,6 @@
   14.15  
   14.16  (* basics *)
   14.17  
   14.18 -val exhaustive_plugin = "quickcheck_exhaustive"
   14.19 -val bounded_forall_plugin = "quickcheck_bounded_forall"
   14.20 -val full_exhaustive_plugin = "quickcheck_full_exhaustive"
   14.21 -
   14.22 -
   14.23  (** dynamic options **)
   14.24  
   14.25  val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true)
   14.26 @@ -544,11 +535,11 @@
   14.27  (* setup *)
   14.28  
   14.29  val setup_exhaustive_datatype_interpretation =
   14.30 -  Quickcheck_Common.datatype_interpretation exhaustive_plugin
   14.31 +  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_exhaustive}
   14.32      (@{sort exhaustive}, instantiate_exhaustive_datatype)
   14.33  
   14.34  val setup_bounded_forall_datatype_interpretation =
   14.35 -  BNF_LFP_Compat.interpretation bounded_forall_plugin Quickcheck_Common.compat_prefs
   14.36 +  BNF_LFP_Compat.interpretation @{plugin quickcheck_bounded_forall} Quickcheck_Common.compat_prefs
   14.37      (Quickcheck_Common.ensure_sort
   14.38         (((@{sort type}, @{sort type}), @{sort bounded_forall}),
   14.39         (fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs,
   14.40 @@ -557,7 +548,7 @@
   14.41  val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
   14.42  
   14.43  val setup =
   14.44 -  Quickcheck_Common.datatype_interpretation full_exhaustive_plugin
   14.45 +  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive}
   14.46      (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
   14.47    #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
   14.48    #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
    15.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Oct 13 17:04:25 2014 +0200
    15.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Oct 13 18:45:48 2014 +0200
    15.3 @@ -6,7 +6,6 @@
    15.4  
    15.5  signature NARROWING_GENERATORS =
    15.6  sig
    15.7 -  val narrowing_plugin: string
    15.8    val allow_existentials : bool Config.T
    15.9    val finite_functions : bool Config.T
   15.10    val overlord : bool Config.T
   15.11 @@ -23,8 +22,6 @@
   15.12  structure Narrowing_Generators : NARROWING_GENERATORS =
   15.13  struct
   15.14  
   15.15 -val narrowing_plugin = "quickcheck_narrowing"
   15.16 -
   15.17  (* configurations *)
   15.18  
   15.19  val allow_existentials = Attrib.setup_config_bool @{binding quickcheck_allow_existentials} (K true)
   15.20 @@ -528,7 +525,7 @@
   15.21  val setup =
   15.22    Code.datatype_interpretation ensure_partial_term_of
   15.23    #> Code.datatype_interpretation ensure_partial_term_of_code
   15.24 -  #> Quickcheck_Common.datatype_interpretation narrowing_plugin
   15.25 +  #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
   15.26      (@{sort narrowing}, instantiate_narrowing_datatype)
   15.27    #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
   15.28      
    16.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Oct 13 17:04:25 2014 +0200
    16.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Oct 13 18:45:48 2014 +0200
    16.3 @@ -7,7 +7,6 @@
    16.4  signature RANDOM_GENERATORS =
    16.5  sig
    16.6    type seed = Random_Engine.seed
    16.7 -  val random_plugin: string
    16.8    val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
    16.9      -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
   16.10      -> seed -> (('a -> 'b) * (unit -> term)) * seed
   16.11 @@ -25,8 +24,6 @@
   16.12  structure Random_Generators : RANDOM_GENERATORS =
   16.13  struct
   16.14  
   16.15 -val random_plugin = "quickcheck_random";
   16.16 -
   16.17  (** abstract syntax **)
   16.18  
   16.19  fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
   16.20 @@ -473,7 +470,7 @@
   16.21  val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
   16.22  
   16.23  val setup =
   16.24 -  Quickcheck_Common.datatype_interpretation random_plugin
   16.25 +  Quickcheck_Common.datatype_interpretation @{plugin quickcheck_random}
   16.26      (@{sort random}, instantiate_random_datatype)
   16.27    #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
   16.28  
    17.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Oct 13 17:04:25 2014 +0200
    17.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Oct 13 18:45:48 2014 +0200
    17.3 @@ -6,7 +6,6 @@
    17.4  
    17.5  signature TRANSFER_BNF =
    17.6  sig
    17.7 -  val transfer_plugin: string
    17.8    val base_name_of_bnf: BNF_Def.bnf -> binding
    17.9    val type_name_of_bnf: BNF_Def.bnf -> string
   17.10    val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
   17.11 @@ -21,8 +20,6 @@
   17.12  open BNF_FP_Util
   17.13  open BNF_FP_Def_Sugar
   17.14  
   17.15 -val transfer_plugin = "transfer"
   17.16 -
   17.17  (* util functions *)
   17.18  
   17.19  fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
   17.20 @@ -282,6 +279,8 @@
   17.21  
   17.22  (* BNF interpretation *)
   17.23  
   17.24 +val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}
   17.25 +
   17.26  fun transfer_bnf_interpretation bnf lthy =
   17.27    let
   17.28      val dead = dead_of_bnf bnf
   17.29 @@ -294,9 +293,9 @@
   17.30      |> predicator bnf
   17.31    end
   17.32  
   17.33 -val _ = Theory.setup (bnf_interpretation transfer_plugin
   17.34 -  (bnf_only_type_ctr (BNF_Util.map_local_theory o transfer_bnf_interpretation))
   17.35 -  (bnf_only_type_ctr transfer_bnf_interpretation))
   17.36 +val _ =
   17.37 +  Theory.setup
   17.38 +    (bnf_interpretation transfer_plugin (bnf_only_type_ctr transfer_bnf_interpretation))
   17.39  
   17.40  (* simplification rules for the predicator *)
   17.41  
   17.42 @@ -370,8 +369,8 @@
   17.43      snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
   17.44    end
   17.45  
   17.46 -val _ = Theory.setup (fp_sugars_interpretation transfer_plugin
   17.47 -  (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugars_interpretation))
   17.48 -  (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
   17.49 +val _ =
   17.50 +  Theory.setup (fp_sugars_interpretation transfer_plugin
   17.51 +    (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
   17.52  
   17.53  end
    18.1 --- a/src/HOL/Tools/datatype_realizer.ML	Mon Oct 13 17:04:25 2014 +0200
    18.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Mon Oct 13 18:45:48 2014 +0200
    18.3 @@ -7,15 +7,12 @@
    18.4  
    18.5  signature DATATYPE_REALIZER =
    18.6  sig
    18.7 -  val extraction_plugin: string
    18.8    val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
    18.9  end;
   18.10  
   18.11  structure Datatype_Realizer : DATATYPE_REALIZER =
   18.12  struct
   18.13  
   18.14 -val extraction_plugin = "extraction";
   18.15 -
   18.16  fun subsets i j =
   18.17    if i <= j then
   18.18      let val is = subsets (i+1) j
   18.19 @@ -241,6 +238,6 @@
   18.20        |> fold_rev (perhaps o try o make_casedists) infos
   18.21      end;
   18.22  
   18.23 -val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin [] add_dt_realizers);
   18.24 +val _ = Theory.setup (BNF_LFP_Compat.interpretation @{plugin extraction} [] add_dt_realizers);
   18.25  
   18.26  end;