generate 'code' attribute only if 'code' plugin is enabled
authorblanchet
Mon Sep 15 10:49:07 2014 +0200 (2014-09-15)
changeset 58335a5a3b576fcfb
parent 58334 7553a1bcecb7
child 58336 a7add8066122
generate 'code' attribute only if 'code' plugin is enabled
src/Doc/Datatypes/Datatypes.thy
src/HOL/Extraction.thy
src/HOL/Nitpick.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Sun Sep 14 22:59:30 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 15 10:49:07 2014 +0200
     1.3 @@ -753,7 +753,9 @@
     1.4  
     1.5  \item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
     1.6  @{thm list.case(1)[no_vars]} \\
     1.7 -@{thm list.case(2)[no_vars]}
     1.8 +@{thm list.case(2)[no_vars]} \\
     1.9 +(The @{text "[code]"} attribute is set by the @{text code} plugin,
    1.10 +Section~\ref{ssec:code-generator}.)
    1.11  
    1.12  \item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\
    1.13  @{thm list.case_cong[no_vars]}
    1.14 @@ -788,7 +790,9 @@
    1.15  
    1.16  \item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
    1.17  @{thm list.sel(1)[no_vars]} \\
    1.18 -@{thm list.sel(2)[no_vars]}
    1.19 +@{thm list.sel(2)[no_vars]} \\
    1.20 +(The @{text "[code]"} attribute is set by the @{text code} plugin,
    1.21 +Section~\ref{ssec:code-generator}.)
    1.22  
    1.23  \item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
    1.24  @{thm list.collapse(1)[no_vars]} \\
    1.25 @@ -829,7 +833,8 @@
    1.26  
    1.27  \noindent
    1.28  In addition, equational versions of @{text t.disc} are registered with the
    1.29 -@{text "[code]"} attribute.
    1.30 +@{text "[code]"} attribute. (The @{text "[code]"} attribute is set by the
    1.31 +@{text code} plugin, Section~\ref{ssec:code-generator}.)
    1.32  *}
    1.33  
    1.34  
    1.35 @@ -857,7 +862,9 @@
    1.36  
    1.37  \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
    1.38  @{thm list.set(1)[no_vars]} \\
    1.39 -@{thm list.set(2)[no_vars]}
    1.40 +@{thm list.set(2)[no_vars]} \\
    1.41 +(The @{text "[code]"} attribute is set by the @{text code} plugin,
    1.42 +Section~\ref{ssec:code-generator}.)
    1.43  
    1.44  \item[@{text "t."}\hthm{set_cases} @{text "[consumes 1, cases set: set\<^sub>i_t]"}\rm:] ~ \\
    1.45  @{thm list.set_cases[no_vars]}
    1.46 @@ -871,7 +878,9 @@
    1.47  
    1.48  \item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
    1.49  @{thm list.map(1)[no_vars]} \\
    1.50 -@{thm list.map(2)[no_vars]}
    1.51 +@{thm list.map(2)[no_vars]} \\
    1.52 +(The @{text "[code]"} attribute is set by the @{text code} plugin,
    1.53 +Section~\ref{ssec:code-generator}.)
    1.54  
    1.55  \item[@{text "t."}\hthm{map_disc_iff} @{text "[simp]"}\rm:] ~ \\
    1.56  @{thm list.map_disc_iff[no_vars]}
    1.57 @@ -903,7 +912,9 @@
    1.58  
    1.59  \noindent
    1.60  In addition, equational versions of @{text t.rel_inject} and @{text
    1.61 -rel_distinct} are registered with the @{text "[code]"} attribute.
    1.62 +rel_distinct} are registered with the @{text "[code]"} attribute. (The
    1.63 +@{text "[code]"} attribute is set by the @{text code} plugin,
    1.64 +Section~\ref{ssec:code-generator}.)
    1.65  
    1.66  The second subgroup consists of more abstract properties of the set functions,
    1.67  the map function, and the relator:
    1.68 @@ -999,7 +1010,9 @@
    1.69  
    1.70  \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
    1.71  @{thm list.rec(1)[no_vars]} \\
    1.72 -@{thm list.rec(2)[no_vars]}
    1.73 +@{thm list.rec(2)[no_vars]} \\
    1.74 +(The @{text "[code]"} attribute is set by the @{text code} plugin,
    1.75 +Section~\ref{ssec:code-generator}.)
    1.76  
    1.77  \end{description}
    1.78  \end{indentblock}
    1.79 @@ -1804,7 +1817,9 @@
    1.80  @{thm llist.corec(2)[no_vars]}
    1.81  
    1.82  \item[@{text "t."}\hthm{corec_code} @{text "[code]"}\rm:] ~ \\
    1.83 -@{thm llist.corec_code[no_vars]}
    1.84 +@{thm llist.corec_code[no_vars]} \\
    1.85 +(The @{text "[code]"} attribute is set by the @{text code} plugin,
    1.86 +Section~\ref{ssec:code-generator}.)
    1.87  
    1.88  \item[@{text "t."}\hthm{corec_disc}\rm:] ~ \\
    1.89  @{thm llist.corec_disc(1)[no_vars]} \\
     2.1 --- a/src/HOL/Extraction.thy	Sun Sep 14 22:59:30 2014 +0200
     2.2 +++ b/src/HOL/Extraction.thy	Mon Sep 15 10:49:07 2014 +0200
     2.3 @@ -37,7 +37,7 @@
     2.4    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
     2.5    induct_true_def induct_false_def
     2.6  
     2.7 -datatype (plugins only: code) sumbool = Left | Right
     2.8 +datatype (plugins only:) sumbool = Left | Right
     2.9  
    2.10  subsection {* Type of extracted program *}
    2.11  
     3.1 --- a/src/HOL/Nitpick.thy	Sun Sep 14 22:59:30 2014 +0200
     3.2 +++ b/src/HOL/Nitpick.thy	Mon Sep 15 10:49:07 2014 +0200
     3.3 @@ -14,9 +14,9 @@
     3.4    "nitpick_params" :: thy_decl
     3.5  begin
     3.6  
     3.7 -datatype (plugins only: code) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
     3.8 -datatype (plugins only: code) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
     3.9 -datatype (plugins only: code) (dead 'a) word = Word "'a set"
    3.10 +datatype (plugins only:) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
    3.11 +datatype (plugins only:) (dead 'a, dead 'b) pair_box = PairBox 'a 'b
    3.12 +datatype (plugins only:) (dead 'a) word = Word "'a set"
    3.13  
    3.14  typedecl bisim_iterator
    3.15  typedecl unsigned_bit
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Sep 14 22:59:30 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 15 10:49:07 2014 +0200
     4.3 @@ -93,7 +93,7 @@
     4.4    val mk_induct_attrs: term list list -> Token.src list
     4.5    val mk_coinduct_attrs: typ list -> term list list -> term list list -> int list list ->
     4.6      Token.src list * Token.src list
     4.7 -  val derive_induct_recs_thms_for_types: BNF_Def.bnf list ->
     4.8 +  val derive_induct_recs_thms_for_types: (string -> bool) -> BNF_Def.bnf list ->
     4.9       ('a * typ list list list list * term list list * 'b) option -> thm -> thm list ->
    4.10       BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list ->
    4.11       typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list ->
    4.12 @@ -311,7 +311,6 @@
    4.13  
    4.14  val fundefcong_attrs = @{attributes [fundef_cong]};
    4.15  val nitpicksimp_attrs = @{attributes [nitpick_simp]};
    4.16 -val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
    4.17  val simp_attrs = @{attributes [simp]};
    4.18  
    4.19  val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
    4.20 @@ -626,7 +625,7 @@
    4.21       mk_induct_attrs ctrAss)
    4.22    end;
    4.23  
    4.24 -fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
    4.25 +fun derive_induct_recs_thms_for_types plugins pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
    4.26      live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions
    4.27      abs_inverses ctrss ctr_defss recs rec_defs lthy =
    4.28    let
    4.29 @@ -763,9 +762,11 @@
    4.30        end;
    4.31  
    4.32      val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
    4.33 +
    4.34 +    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
    4.35    in
    4.36      ((induct_thms, induct_thm, mk_induct_attrs ctrss),
    4.37 -     (rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
    4.38 +     (rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs))
    4.39    end;
    4.40  
    4.41  fun mk_coinduct_attrs fpTs ctrss discss mss =
    4.42 @@ -1364,6 +1365,8 @@
    4.43            fp_b_names fpTs thmss)
    4.44        #> filter_out (null o fst o hd o snd);
    4.45  
    4.46 +    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
    4.47 +
    4.48      val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
    4.49      val ns = map length ctr_Tsss;
    4.50      val kss = map (fn n => 1 upto n) ns;
    4.51 @@ -1923,14 +1926,14 @@
    4.52                  end;
    4.53  
    4.54                val anonymous_notes =
    4.55 -                [(rel_eq_thms, code_nitpicksimp_attrs)]
    4.56 +                [(rel_eq_thms, code_attrs @ nitpicksimp_attrs)]
    4.57                  |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    4.58  
    4.59                val notes =
    4.60                  [(case_transferN, [case_transfer_thms], K []),
    4.61                   (ctr_transferN, ctr_transfer_thms, K []),
    4.62                   (disc_transferN, disc_transfer_thms, K []),
    4.63 -                 (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
    4.64 +                 (mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
    4.65                   (map_disc_iffN, map_disc_iff_thms, K simp_attrs),
    4.66                   (map_selN, map_sel_thms, K []),
    4.67                   (rel_casesN, [rel_cases_thm], K rel_cases_attrs),
    4.68 @@ -1938,7 +1941,7 @@
    4.69                   (rel_injectN, rel_inject_thms, K simp_attrs),
    4.70                   (rel_introsN, rel_intro_thms, K []),
    4.71                   (rel_selN, rel_sel_thms, K []),
    4.72 -                 (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
    4.73 +                 (setN, set_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
    4.74                   (set_casesN, set_cases_thms, nth set_cases_attrss),
    4.75                   (set_introsN, set_intros_thms, K []),
    4.76                   (set_selN, set_sel_thms, K [])]
    4.77 @@ -1985,9 +1988,9 @@
    4.78            (recs, rec_defs)), lthy) =
    4.79        let
    4.80          val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
    4.81 -          derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct xtor_co_rec_thms
    4.82 -            live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
    4.83 -            abs_inverses ctrss ctr_defss recs rec_defs lthy;
    4.84 +          derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct
    4.85 +            xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
    4.86 +            type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
    4.87  
    4.88          val induct_type_attr = Attrib.internal o K o Induct.induct_type;
    4.89          val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
    4.90 @@ -2111,7 +2114,7 @@
    4.91              fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
    4.92             (coinduct_strongN, map single coinduct_strong_thms, K coinduct_attrs),
    4.93             (corecN, corec_thmss, K []),
    4.94 -           (corec_codeN, map single corec_code_thms, K code_nitpicksimp_attrs),
    4.95 +           (corec_codeN, map single corec_code_thms, K (code_attrs @ nitpicksimp_attrs)),
    4.96             (corec_discN, corec_disc_thmss, K []),
    4.97             (corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
    4.98             (corec_selN, corec_sel_thmss, K corec_sel_attrs),
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Sun Sep 14 22:59:30 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 15 10:49:07 2014 +0200
     5.3 @@ -11,13 +11,14 @@
     5.4    val unfold_splits_lets: term -> term
     5.5    val dest_map: Proof.context -> string -> term -> term * term list
     5.6  
     5.7 -  val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
     5.8 -    term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
     5.9 +  val mutualize_fp_sugars: (string -> bool) -> BNF_Util.fp_kind -> int list -> binding list ->
    5.10 +    typ list -> term list -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
    5.11 +    local_theory ->
    5.12      (BNF_FP_Def_Sugar.fp_sugar list
    5.13       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    5.14      * local_theory
    5.15 -  val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
    5.16 -    (term * term list list) list list -> local_theory ->
    5.17 +  val nested_to_mutual_fps: (string -> bool) -> BNF_Util.fp_kind -> binding list -> typ list ->
    5.18 +    term list -> (term * term list list) list list -> local_theory ->
    5.19      (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
    5.20       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    5.21      * local_theory
    5.22 @@ -116,7 +117,7 @@
    5.23    |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
    5.24    |> map_filter I;
    5.25  
    5.26 -fun mutualize_fp_sugars fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy =
    5.27 +fun mutualize_fp_sugars plugins fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy =
    5.28    let
    5.29      val thy = Proof_Context.theory_of no_defs_lthy;
    5.30  
    5.31 @@ -269,7 +270,7 @@
    5.32          val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss),
    5.33               fp_sugar_thms) =
    5.34            if fp = Least_FP then
    5.35 -            derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
    5.36 +            derive_induct_recs_thms_for_types plugins pre_bnfs recs_args_types xtor_co_induct
    5.37                xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
    5.38                fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs
    5.39                lthy
    5.40 @@ -332,7 +333,7 @@
    5.41  
    5.42  val impossible_caller = Bound ~1;
    5.43  
    5.44 -fun nested_to_mutual_fps fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
    5.45 +fun nested_to_mutual_fps plugins fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
    5.46    let
    5.47      val qsoty = quote o Syntax.string_of_typ lthy;
    5.48      val qsotys = space_implode " or " o map qsoty;
    5.49 @@ -456,8 +457,8 @@
    5.50        if length perm_Tss = 1 then
    5.51          ((perm_fp_sugars0, (NONE, NONE)), lthy)
    5.52        else
    5.53 -        mutualize_fp_sugars fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers perm_callssss
    5.54 -          perm_fp_sugars0 lthy;
    5.55 +        mutualize_fp_sugars plugins fp perm_cliques perm_bs perm_frozen_gen_Ts perm_callers
    5.56 +          perm_callssss perm_fp_sugars0 lthy;
    5.57  
    5.58      val fp_sugars = unpermute perm_fp_sugars;
    5.59    in
     6.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sun Sep 14 22:59:30 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Sep 15 10:49:07 2014 +0200
     6.3 @@ -409,7 +409,7 @@
     6.4  
     6.5      val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
     6.6            common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
     6.7 -      nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
     6.8 +      nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0;
     6.9  
    6.10      val coinduct_attrs_pair =
    6.11        (case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], []));
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sun Sep 14 22:59:30 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 15 10:49:07 2014 +0200
     7.3 @@ -286,7 +286,8 @@
     7.4  
     7.5      val ((fp_sugars', (lfp_sugar_thms', _)), lthy') =
     7.6        if nn > nn_fp then
     7.7 -        mutualize_fp_sugars Least_FP cliques compat_bs fpTs' callers callssss fp_sugars lthy
     7.8 +        mutualize_fp_sugars (K true) Least_FP cliques compat_bs fpTs' callers callssss fp_sugars
     7.9 +          lthy
    7.10        else
    7.11          ((fp_sugars, (NONE, NONE)), lthy);
    7.12  
     8.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Sun Sep 14 22:59:30 2014 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Mon Sep 15 10:49:07 2014 +0200
     8.3 @@ -31,7 +31,7 @@
     8.4      val ((missing_arg_Ts, perm0_kks,
     8.5            fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
     8.6            (lfp_sugar_thms, _)), lthy) =
     8.7 -      nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
     8.8 +      nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
     8.9  
    8.10      val induct_attrs = (case lfp_sugar_thms of SOME ((_, _, attrs), _) => attrs | NONE => []);
    8.11  
     9.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Sun Sep 14 22:59:30 2014 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 15 10:49:07 2014 +0200
     9.3 @@ -32,7 +32,6 @@
     9.4  
     9.5  val nitpicksimp_attrs = @{attributes [nitpick_simp]};
     9.6  val simp_attrs = @{attributes [simp]};
     9.7 -val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
     9.8  
     9.9  structure Data = Generic_Data
    9.10  (
    9.11 @@ -346,6 +345,9 @@
    9.12              (map single rec_o_map_thms, size_o_map_thmss)
    9.13            end;
    9.14  
    9.15 +      (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *)
    9.16 +      val code_attrs = Code.add_default_eqn_attrib;
    9.17 +
    9.18        val massage_multi_notes =
    9.19          maps (fn (thmN, thmss, attrs) =>
    9.20            map2 (fn T_name => fn thms =>
    9.21 @@ -356,7 +358,7 @@
    9.22  
    9.23        val notes =
    9.24          [(rec_o_mapN, rec_o_map_thmss, []),
    9.25 -         (sizeN, size_thmss, code_nitpicksimp_simp_attrs),
    9.26 +         (sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
    9.27           (size_o_mapN, size_o_map_thmss, [])]
    9.28          |> massage_multi_notes;
    9.29  
    10.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun Sep 14 22:59:30 2014 +0200
    10.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 15 10:49:07 2014 +0200
    10.3 @@ -91,7 +91,7 @@
    10.4  open Ctr_Sugar_Tactics
    10.5  open Ctr_Sugar_Code
    10.6  
    10.7 -val code_plugin = "code"
    10.8 +val code_plugin = "code";
    10.9  
   10.10  type ctr_sugar =
   10.11    {T: typ,
   10.12 @@ -250,8 +250,6 @@
   10.13  val inductsimp_attrs = @{attributes [induct_simp]};
   10.14  val nitpicksimp_attrs = @{attributes [nitpick_simp]};
   10.15  val simp_attrs = @{attributes [simp]};
   10.16 -val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
   10.17 -val code_nitpicksimp_simp_attrs = code_nitpicksimp_attrs @ simp_attrs;
   10.18  
   10.19  fun unflat_lookup eq xs ys = map (fn xs' => permute_like_unique eq xs xs' ys);
   10.20  
   10.21 @@ -978,17 +976,19 @@
   10.22          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
   10.23          val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
   10.24  
   10.25 +        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
   10.26 +
   10.27          val nontriv_disc_eq_thmss =
   10.28            map (map (fn th => th RS @{thm eq_False[THEN iffD2]}
   10.29              handle THM _ => th RS @{thm eq_True[THEN iffD2]})) nontriv_disc_thmss;
   10.30  
   10.31          val anonymous_notes =
   10.32            [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs),
   10.33 -           (flat nontriv_disc_eq_thmss, code_nitpicksimp_attrs)]
   10.34 +           (flat nontriv_disc_eq_thmss, code_attrs @ nitpicksimp_attrs)]
   10.35            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   10.36  
   10.37          val notes =
   10.38 -          [(caseN, case_thms, code_nitpicksimp_simp_attrs),
   10.39 +          [(caseN, case_thms, code_attrs @ nitpicksimp_attrs @ simp_attrs),
   10.40             (case_congN, [case_cong_thm], []),
   10.41             (case_cong_weak_thmsN, [case_cong_weak_thm], cong_attrs),
   10.42             (case_eq_ifN, case_eq_if_thms, []),
   10.43 @@ -1003,7 +1003,7 @@
   10.44             (expandN, expand_thms, []),
   10.45             (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
   10.46             (nchotomyN, [nchotomy_thm], []),
   10.47 -           (selN, all_sel_thms, code_nitpicksimp_simp_attrs),
   10.48 +           (selN, all_sel_thms, code_attrs @ nitpicksimp_attrs @ simp_attrs),
   10.49             (splitN, [split_thm], []),
   10.50             (split_asmN, [split_asm_thm], []),
   10.51             (split_selN, split_sel_thms, []),
   10.52 @@ -1022,16 +1022,16 @@
   10.53            |> fold (Spec_Rules.add Spec_Rules.Equational)
   10.54              (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
   10.55            |> Local_Theory.declaration {syntax = false, pervasive = true}
   10.56 -               (fn phi => Case_Translation.register
   10.57 -                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
   10.58 +            (fn phi => Case_Translation.register
   10.59 +               (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
   10.60            |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
   10.61            |> plugins code_plugin ?
   10.62 -             Local_Theory.declaration {syntax = false, pervasive = false}
   10.63 -               (fn phi => Context.mapping
   10.64 -                  (add_ctr_code fcT_name (map (Morphism.typ phi) As)
   10.65 -                     (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
   10.66 -                     (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
   10.67 -                  I)
   10.68 +            Local_Theory.declaration {syntax = false, pervasive = false}
   10.69 +              (fn phi => Context.mapping
   10.70 +                 (add_ctr_code fcT_name (map (Morphism.typ phi) As)
   10.71 +                    (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
   10.72 +                    (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
   10.73 +                 I)
   10.74            |> Local_Theory.notes (anonymous_notes @ notes)
   10.75            (* for "datatype_realizer.ML": *)
   10.76            |>> name_noted_thms fcT_name exhaustN;