# HG changeset patch
# User blanchet
# Date 1420489454 -3600
# Node ID 5ca195783da869c5c12f111655a662a1ae6c4a97
# Parent  c5f6e2c4472cfd619fc99f13220b7a6679f7cd35
generate [code] only with 'code' plugin enabled

diff -r c5f6e2c4472c -r 5ca195783da8 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 05 11:00:12 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jan 05 21:24:14 2015 +0100
@@ -1020,7 +1020,7 @@
                |> map Thm.close_derivation)
         end;
 
-      val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
+      val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
 
       val anonymous_notes =
         [(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
@@ -1455,7 +1455,7 @@
 
     val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
 
-    val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
+    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
   in
     ((induct_thms, induct_thm, mk_induct_attrs ctrss),
      (rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs))
@@ -2081,7 +2081,7 @@
     val fpTs = map (domain_type o fastype_of) dtors;
     val fpBTs = map B_ify_T fpTs;
 
-    val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
+    val code_attrs = if plugins code_plugin 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;
diff -r c5f6e2c4472c -r 5ca195783da8 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jan 05 11:00:12 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jan 05 21:24:14 2015 +0100
@@ -83,7 +83,6 @@
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
-val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
 
 exception PRIMCOREC of string * term list;
 
@@ -1413,6 +1412,8 @@
 
         val common_name = mk_common_name fun_names;
 
+        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+
         val anonymous_notes =
           [(flat disc_iff_or_disc_thmss, simp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
@@ -1428,7 +1429,7 @@
           [(coinductN, map (if n2m then single else K []) coinduct_thms, coinduct_attrs),
            (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms,
             coinduct_attrs),
-           (codeN, code_thmss, code_nitpicksimp_attrs),
+           (codeN, code_thmss, code_attrs @ nitpicksimp_attrs),
            (ctrN, ctr_thmss, []),
            (discN, disc_thmss, []),
            (disc_iffN, disc_iff_thmss, []),
diff -r c5f6e2c4472c -r 5ca195783da8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jan 05 11:00:12 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jan 05 21:24:14 2015 +0100
@@ -89,7 +89,7 @@
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
-val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
+val nitpicksimp_simp_attrs = nitpicksimp_attrs @ simp_attrs;
 
 exception OLD_PRIMREC of unit;
 exception PRIMREC of string * term list;
@@ -438,7 +438,7 @@
       else warning ("no equation for constructor " ^ Syntax.string_of_term ctxt ctr));
 
     val ctr_spec_eqn_data_list =
-      map (fn ((x, y), z) => (x, z)) ctr_spec_eqn_data_list' @
+      map (apfst fst) ctr_spec_eqn_data_list' @
         (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair []));
 
     val recs = take n_funs rec_specs |> map #recx;
@@ -548,13 +548,12 @@
         val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
           |> fst
           |> map_filter (try (fn (x, [y]) =>
-            (#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
-          |> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) =>
+            (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
+          |> map (fn (user_eqn, num_extra_args, rec_thm) =>
               mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
                 def_thms rec_thm
               |> K |> Goal.prove_sorry lthy' [] [] user_eqn
-              |> Thm.close_derivation)
-            js;
+              |> Thm.close_derivation);
       in
         ((js, simp_thms), lthy')
       end;
@@ -591,14 +590,12 @@
       lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
   end;
 
-fun add_primrec_simple' opts fixes ts lthy =
+fun add_primrec_simple0 plugins nonexhaustive transfer fixes ts lthy =
   let
     val actual_nn = length fixes;
 
-    val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
-      |> the_default Plugin_Name.default_filter;
-    val nonexhaustives = replicate actual_nn (exists (can (fn Nonexhaustive_Option => ())) opts);
-    val transfers = replicate actual_nn (exists (can (fn Transfer_Option => ())) opts);
+    val nonexhaustives = replicate actual_nn nonexhaustive;
+    val transfers = replicate actual_nn transfer;
 
     val (((names, defs), prove), lthy') =
       prepare_primrec plugins nonexhaustives transfers fixes ts lthy
@@ -618,7 +615,7 @@
              space_implode "\n  " (map (quote o Syntax.string_of_term lthy) eqns));
 
 fun add_primrec_simple fixes ts lthy =
-  add_primrec_simple' [] fixes ts lthy
+  add_primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy
   handle OLD_PRIMREC () =>
     Old_Primrec.add_primrec_simple fixes ts lthy
     |>> apsnd (apsnd (pair [] o single)) o apfst single;
@@ -626,9 +623,16 @@
 fun gen_primrec old_primrec prep_spec opts
     (raw_fixes : (binding * 'a option * mixfix) list) raw_specs lthy =
   let
-    val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes)
+    val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes);
     val _ = null d orelse raise PRIMREC ("duplicate function name(s): " ^ commas d, []);
 
+    val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
+      |> the_default Plugin_Name.default_filter;
+    val nonexhaustive = exists (can (fn Nonexhaustive_Option => ())) opts;
+    val transfer = exists (can (fn Transfer_Option => ())) opts;
+
+    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+
     val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
 
     val mk_notes =
@@ -637,7 +641,7 @@
           val (bs, attrss) = map_split (fst o nth specs) js;
           val notes =
             @{map 3} (fn b => fn attrs => fn thm =>
-                ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs),
+                ((Binding.qualify false prefix b, code_attrs @ nitpicksimp_simp_attrs @ attrs),
                  [([thm], [])]))
               bs attrss thms;
         in
@@ -645,7 +649,7 @@
         end);
   in
     lthy
-    |> add_primrec_simple' opts fixes (map snd specs)
+    |> add_primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs)
     |-> (fn (names, (ts, (jss, simpss))) =>
       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
       #> Local_Theory.notes (mk_notes jss names simpss)
diff -r c5f6e2c4472c -r 5ca195783da8 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jan 05 11:00:12 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jan 05 21:24:14 2015 +0100
@@ -75,6 +75,8 @@
   val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c
   val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
 
+  val code_plugin: string
+
   type ctr_options = (string -> bool) * bool
   type ctr_options_cmd = (Proof.context -> string -> bool) * bool