added 'plugins' option to control which hooks are enabled

--- a/src/HOL/Library/bnf_axiomatization.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -7,8 +7,8 @@
 
 signature BNF_AXIOMATIZATION =
 sig
-  val bnf_axiomatization: (binding option * (typ * sort)) list -> binding -> mixfix -> binding ->
-    binding -> typ list -> local_theory -> BNF_Def.bnf * local_theory
+  val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding ->
+    mixfix -> binding -> binding -> typ list -> local_theory -> BNF_Def.bnf * local_theory
 end
 
 structure BNF_Axiomatization : BNF_AXIOMATIZATION =
@@ -17,7 +17,8 @@
 open BNF_Util
 open BNF_Def
 
-fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy =
+fun prepare_decl prepare_constraint prepare_typ plugins raw_vars b mx user_mapb user_relb user_witTs
+  lthy =
   let
    fun prepare_type_arg (set_opt, (ty, c)) =
       let val s = fst (dest_TFree (prepare_typ lthy ty)) in
@@ -46,14 +47,14 @@
     val mapT = map2 (curry op -->) lives lives' ---> T --> T';
     val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
     val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
-    val mapb = mk_b BNF_Def.mapN user_mapb;
+    val mapb = mk_b mapN user_mapb;
     val bdb = mk_b "bd" Binding.empty;
-    val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs
+    val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs
       (if live = 1 then [0] else 1 upto live);
 
     val witTs = map (prepare_typ lthy) user_witTs;
     val nwits = length witTs;
-    val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty)
+    val witbs = map (fn i => mk_b (mk_witN i) Binding.empty)
       (if nwits = 1 then [0] else 1 upto nwits);
 
     val lthy = Local_Theory.background_theory
@@ -91,7 +92,7 @@
 
     val (bnf, lthy') = after_qed mk_wit_thms thms lthy
   in
-    (bnf, BNF_Def.register_bnf (K true) key bnf lthy')
+    (bnf, register_bnf plugins key bnf lthy')
   end;
 
 val bnf_axiomatization = prepare_decl (K I) (K I);
@@ -107,14 +108,17 @@
          | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
   @{keyword "]"} || Scan.succeed [];
 
+val parse_bnf_axiomatization_options =
+  Scan.optional (@{keyword "("} |-- parse_plugins --| @{keyword ")"}) (K true);
+
 val parse_bnf_axiomatization =
-  parse_type_args_named_constrained -- Parse.binding -- parse_witTs -- Parse.opt_mixfix --
-  parse_map_rel_bindings;
+  parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding --
+  parse_witTs -- Parse.opt_mixfix -- parse_map_rel_bindings;
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration"
     (parse_bnf_axiomatization >> 
-      (fn ((((bsTs, b), witTs), mx), (mapb, relb)) =>
-         bnf_axiomatization_cmd bsTs b mx mapb relb witTs #> snd));
+      (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb)) =>
+         bnf_axiomatization_cmd plugins bsTs b mx mapb relb witTs #> snd));
 
 end;

--- a/src/HOL/Nat.thy	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Nat.thy	Fri Sep 05 00:41:01 2014 +0200
@@ -89,12 +89,12 @@
   | Suc pred
 where
   "pred (0 \<Colon> nat) = (0 \<Colon> nat)"
-  apply atomize_elim
-  apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
- apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
-   Suc_Rep_inject' Rep_Nat_inject)
-apply (simp only: Suc_not_Zero)
-done
+    apply atomize_elim
+    apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
+   apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject'
+     Rep_Nat_inject)
+  apply (simp only: Suc_not_Zero)
+  done
 
 -- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
 setup {* Sign.mandatory_path "old" *}

--- a/src/HOL/Product_Type.thy	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Product_Type.thy	Fri Sep 05 00:41:01 2014 +0200
@@ -13,7 +13,7 @@
 subsection {* @{typ bool} is a datatype *}
 
 free_constructors case_bool for True | False
-by auto
+  by auto
 
 text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
 
@@ -82,7 +82,7 @@
 *}
 
 free_constructors case_unit for "()"
-by auto
+  by auto
 
 text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
 

--- a/src/HOL/Sum_Type.thy	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Sum_Type.thy	Fri Sep 05 00:41:01 2014 +0200
@@ -88,7 +88,7 @@
 free_constructors case_sum for
     isl: Inl projl
   | Inr projr
-by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
+  by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
 
 text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
 

--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -122,11 +122,9 @@
     (binding -> binding) -> (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) ->
     typ list option -> binding -> binding -> binding list ->
     (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
-    string * term list *
-    ((Proof.context -> thm list -> tactic) option * term list list) *
+    string * term list * ((Proof.context -> thm list -> tactic) option * term list list) *
     ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
     local_theory * thm list
-
   val define_bnf_consts: inline_policy -> fact_policy -> bool -> typ list option ->
     binding -> binding -> binding list ->
     (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
@@ -140,11 +138,10 @@
         (typ list -> typ list -> typ list -> term))) * local_theory
 
   val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> bool -> (binding -> binding) ->
-    (Proof.context -> tactic) list ->
-    (Proof.context -> tactic) -> typ list option -> binding ->
+    (Proof.context -> tactic) list -> (Proof.context -> tactic) -> typ list option -> binding ->
     binding -> binding list ->
-    (((((binding * typ) * term) * term list) * term) * term list) * term option ->
-    local_theory -> bnf * local_theory
+    (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
+    bnf * local_theory
 end;
 
 structure BNF_Def : BNF_DEF =
@@ -1532,10 +1529,10 @@
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
 
-fun register_bnf keep key bnf =
-  register_bnf_raw key bnf #> interpret_bnf keep bnf;
+fun register_bnf plugins key bnf =
+  register_bnf_raw key bnf #> interpret_bnf plugins bnf;
 
-fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
+fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs raw_csts =
   (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
   let
     fun mk_wits_tac ctxt set_maps =
@@ -1555,9 +1552,11 @@
       goals (map (fn tac => fn {context = ctxt, prems = _} =>
         unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
     |> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
-  end) oo prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs;
+  end) o prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs
+    raw_csts;
 
-val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
+fun bnf_cmd (raw_csts, plugins) =
+  (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
   let
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
     fun mk_triv_wit_thms tac set_maps =
@@ -1572,10 +1571,10 @@
       | SOME tac => (mk_triv_wit_thms tac, []));
   in
     Proof.unfolding ([[(defs, [])]])
-      (Proof.theorem NONE (uncurry (register_bnf (K true) key) oo after_qed mk_wit_thms)
+      (Proof.theorem NONE (uncurry (register_bnf plugins key) oo after_qed mk_wit_thms)
         (map (single o rpair []) goals @ nontriv_wit_goals) lthy)
-  end) oo prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
-    NONE Binding.empty Binding.empty [];
+  end) o prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
+    NONE Binding.empty Binding.empty [] raw_csts;
 
 fun print_bnfs ctxt =
   let
@@ -1611,12 +1610,13 @@
     "register a type as a bounded natural functor"
     (parse_opt_binding_colon -- Parse.typ --|
        (Parse.reserved "map" -- @{keyword ":"}) -- Parse.term --
-       (Scan.option ((Parse.reserved "sets" -- @{keyword ":"}) |--
-         Scan.repeat1 (Scan.unless (Parse.reserved "bd") Parse.term)) >> the_default []) --|
+       Scan.optional ((Parse.reserved "sets" -- @{keyword ":"}) |--
+         Scan.repeat1 (Scan.unless (Parse.reserved "bd") Parse.term)) [] --|
        (Parse.reserved "bd" -- @{keyword ":"}) -- Parse.term --
-       (Scan.option ((Parse.reserved "wits" -- @{keyword ":"}) |--
-         Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) >> the_default []) --
-       Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term)
+       Scan.optional ((Parse.reserved "wits" -- @{keyword ":"}) |--
+         Scan.repeat1 (Scan.unless (Parse.reserved "rel") Parse.term)) [] --
+       Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) --
+       Scan.optional parse_plugins (K true)
        >> bnf_cmd);
 
 val _ = Context.>> (Context.map_theory BNF_Interpretation.init);

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -104,7 +104,7 @@
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
       BNF_FP_Util.fp_result * local_theory) ->
-    (bool * bool)
+    Ctr_Sugar.ctr_options
     * ((((((binding option * (typ * sort)) list * binding) * mixfix)
          * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * (binding * binding))
        * term list) list ->
@@ -236,10 +236,10 @@
         (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
     fp_sugars;
 
-fun register_fp_sugars keep fp_sugars =
-  register_fp_sugars_raw fp_sugars #> interpret_fp_sugars keep fp_sugars;
+fun register_fp_sugars plugins fp_sugars =
+  register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars;
 
-fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
+fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
     live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss
     common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
     rel_distinctss noted =
@@ -258,8 +258,8 @@
         |> morph_fp_sugar (substitute_noted_thm noted)) Ts;
   in
     register_fp_sugars_raw fp_sugars
-    #> fold (interpret_bnf (K true)) (#bnfs fp_res)
-    #> interpret_fp_sugars (K true) fp_sugars
+    #> fold (interpret_bnf plugins) (#bnfs fp_res)
+    #> interpret_fp_sugars plugins fp_sugars
   end;
 
 (* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A",
@@ -1166,7 +1166,7 @@
   end;
 
 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
-    ((discs_sels0, no_code), specs) no_defs_lthy0 =
+    ((plugins, (discs_sels0, no_code)), specs) no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
 
@@ -1458,8 +1458,8 @@
             fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
             val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;
           in
-            free_constructors tacss ((((discs_sels, no_code), standard_binding), ctr_specs),
-              sel_default_eqs) lthy
+            free_constructors tacss ((((plugins, (discs_sels, no_code)), standard_binding),
+              ctr_specs), sel_default_eqs) lthy
           end;
 
         fun derive_maps_sets_rels (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs,
@@ -2054,7 +2054,7 @@
         (* for "datatype_realizer.ML": *)
         |>> name_noted_thms
           (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN
-        |-> interpret_bnfs_register_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
+        |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
           mapss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn [])
           rel_injectss rel_distinctss
@@ -2146,7 +2146,7 @@
         |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
           [flat corec_sel_thmss, flat corec_thmss]
         |> Local_Theory.notes (common_notes @ notes)
-        |-> interpret_bnfs_register_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos
+        |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs
           mapss [coinduct_thm, coinduct_strong_thm]
           (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -357,7 +357,7 @@
   in
     (fpT_names,
      thy
-     |> map_local_theory (co_datatypes Least_FP construct_lfp ((false, false), new_specs))
+     |> map_local_theory (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs))
      |> nesting_pref = Unfold_Nesting ? perhaps (try (datatype_compat_global fpT_names)))
   end;
 

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -69,12 +69,15 @@
   val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c
   val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
 
+  type ctr_options = (string -> bool) * (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 ->
-    (((bool * bool) * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
+    ((ctr_options * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
     ctr_sugar * local_theory
+  val default_ctr_options: ctr_options
   val parse_bound_term: (binding * string) parser
-  val parse_ctr_options: (bool * bool) parser
+  val parse_ctr_options: ctr_options parser
   val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a) ctr_spec parser
   val parse_sel_default_eqs: string list parser
 end;
@@ -193,17 +196,17 @@
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update (s, morph_ctr_sugar phi ctr_sugar)));
 
-fun register_ctr_sugar keep ctr_sugar =
-  register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar keep ctr_sugar;
+fun register_ctr_sugar plugins ctr_sugar =
+  register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar plugins ctr_sugar;
 
-fun default_register_ctr_sugar_global keep (ctr_sugar as {T = Type (s, _), ...}) thy =
+fun default_register_ctr_sugar_global plugins (ctr_sugar as {T = Type (s, _), ...}) thy =
   let val tab = Data.get (Context.Theory thy) in
     if Symtab.defined tab s then
       thy
     else
       thy
       |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
-      |> Ctr_Sugar_Interpretation.data_global keep ctr_sugar
+      |> Ctr_Sugar_Interpretation.data_global plugins ctr_sugar
   end;
 
 val isN = "is_";
@@ -359,8 +362,8 @@
 fun ctr_of_ctr_spec ((_, ctr), _) = ctr;
 fun args_of_ctr_spec (_, args) = args;
 
-fun prepare_free_constructors prep_term
-    ((((discs_sels, no_code), raw_case_binding), ctr_specs), sel_default_eqs) no_defs_lthy =
+fun prepare_free_constructors prep_term ((((plugins, (discs_sels, no_code)), raw_case_binding),
+    ctr_specs), sel_default_eqs) no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
 
@@ -1045,7 +1048,7 @@
            case_eq_ifs = case_eq_if_thms}
           |> morph_ctr_sugar (substitute_noted_thm noted);
       in
-        (ctr_sugar, lthy' |> register_ctr_sugar (K true) ctr_sugar)
+        (ctr_sugar, lthy' |> register_ctr_sugar plugins ctr_sugar)
       end;
   in
     (goalss, after_qed, lthy')
@@ -1061,12 +1064,18 @@
 
 val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
 
+type ctr_options = (string -> bool) * (bool * bool)
+
+val default_ctr_options = (K true, (false, false));
+
 val parse_ctr_options =
   Scan.optional (@{keyword "("} |-- Parse.list1
-        (Parse.reserved "discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
+        (parse_plugins >> (apfst o K)
+         || Parse.reserved "discs_sels" >> (apsnd o apfst o K o K true)
+         || Parse.reserved "no_code" >> (apsnd o apsnd o K o K true)) --|
       @{keyword ")"}
-      >> (fn js => (member (op =) js 0, member (op =) js 1)))
-    (false, false);
+      >> (fn fs => fold I fs default_ctr_options))
+    default_ctr_options;
 
 fun parse_ctr_spec parse_ctr parse_arg =
   parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg;

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -76,6 +76,7 @@
   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
 
@@ -268,6 +269,11 @@
 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) >> (fn (modif, ss) => modif o member (op =) ss);
+
 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*)