--- 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], []),