src/HOL/BNF/Tools/bnf_ctr_sugar.ML

 val cong_attrs = @{attributes [cong]};
 val safe_elim_attrs = @{attributes [elim!]};
 val iff_attrs = @{attributes [iff]};
 val induct_simp_attrs = @{attributes [induct_simp]};
 val simp_attrs = @{attributes [simp]};
+val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
 
 fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
 
 fun mk_half_pairss' _ ([], []) = []
   | mk_half_pairss' indent (x :: xs, _ :: ys) =

 
         val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
         val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
 
         val notes =
-          [(caseN, case_thms, simp_attrs),
+          [(caseN, case_thms, code_simp_attrs),
            (case_congN, [case_cong_thm], []),
            (case_convN, case_conv_thms, []),
            (collapseN, safe_collapse_thms, simp_attrs),
            (discN, nontriv_disc_thms, simp_attrs),
            (discIN, nontriv_discI_thms, []),