src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

 open BNF_Util
 open BNF_FP_Util
 open BNF_FP_Rec_Sugar_Util
 open BNF_FP_Rec_Sugar_Tactics
 
+val codeN = "code"
 val ctrN = "ctr"
 val discN = "disc"
 val selN = "sel"
 
+val nitpick_attrs = @{attributes [nitpick_simp]};
+val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs;
 val simp_attrs = @{attributes [simp]};
 
 exception Primrec_Error of string * term list;
 
 fun primrec_error str = raise Primrec_Error (str, []);

             mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
             |> K |> Goal.prove lthy [] [] user_eqn)
 
         val notes =
           [(inductN, if nontriv then [induct_thm] else [], []),
-           (simpsN, simp_thms, simp_attrs)]
+           (simpsN, simp_thms, code_nitpick_simp_attrs @ simp_attrs)]
           |> filter_out (null o #2)
           |> map (fn (thmN, thms, attrs) =>
             ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]));
       in
         lthy |> Local_Theory.notes notes

           [(flat safe_ctr_thmss, simp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
         val notes =
           [(coinductN, map (if nontriv then single else K []) coinduct_thms, []),
+           (codeN, ctr_thmss(*FIXME*), code_nitpick_simp_attrs),
            (ctrN, ctr_thmss, []),
            (discN, disc_thmss, simp_attrs),
            (selN, sel_thmss, simp_attrs),
            (simpsN, simp_thmss, []),
            (strong_coinductN, map (if nontriv then single else K []) strong_coinduct_thms, [])]