# HG changeset patch
# User blanchet
# Date 1379974259 -7200
# Node ID 69e8ba502eda71a70830c9a5b5037d13ab8bc94c
# Parent  2c0e45bb2f05ae4b779179b6b251420d2848a6ed
tuning

diff -r 2c0e45bb2f05 -r 69e8ba502eda src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Tue Sep 24 00:10:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Tue Sep 24 00:10:59 2013 +0200
@@ -134,7 +134,7 @@
 val induct_simp_attrs = @{attributes [induct_simp]};
 val nitpick_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
-val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs @ simp_attrs;
+val code_nitpick_simp_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs @ simp_attrs;
 
 fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
 
@@ -760,7 +760,7 @@
         val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
 
         val notes =
-          [(caseN, case_thms, code_nitpick_simp_attrs),
+          [(caseN, case_thms, code_nitpick_simp_simp_attrs),
            (case_congN, [case_cong_thm], []),
            (case_convN, case_conv_thms, []),
            (collapseN, safe_collapse_thms, simp_attrs),
@@ -773,7 +773,7 @@
            (expandN, expand_thms, []),
            (injectN, inject_thms, iff_attrs @ induct_simp_attrs),
            (nchotomyN, [nchotomy_thm], []),
-           (selN, all_sel_thms, code_nitpick_simp_attrs),
+           (selN, all_sel_thms, code_nitpick_simp_simp_attrs),
            (splitN, [split_thm], []),
            (split_asmN, [split_asm_thm], []),
            (splitsN, [split_thm, split_asm_thm], []),