src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 10:35:55 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 10:35:56 2013 +0200
@@ -39,10 +39,10 @@
 val discN = "disc";
 val selN = "sel";
 
-val nitpick_attrs = @{attributes [nitpick_simp]};
+val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
-val code_nitpick_attrs = Code.add_default_eqn_attrib :: nitpick_attrs;
-val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs @ simp_attrs;
+val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
+val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
 
 exception Primrec_Error of string * term list;
 
@@ -407,7 +407,7 @@
           val (bs, attrss) = map_split (fst o nth specs) poss;
           val notes =
             map3 (fn b => fn attrs => fn thm =>
-              ((Binding.qualify false prefix b, code_nitpick_simp_attrs @ attrs), [([thm], [])]))
+              ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs), [([thm], [])]))
             bs attrss thms;
         in
           ((Binding.qualify true prefix (Binding.name simpsN), []), [(thms, [])]) :: notes
@@ -1039,7 +1039,7 @@
 
         val notes =
           [(coinductN, map (if n2m then single else K []) coinduct_thms, []),
-           (codeN, code_thmss, code_nitpick_attrs),
+           (codeN, code_thmss, code_nitpicksimp_attrs),
            (ctrN, ctr_thmss, []),
            (discN, disc_thmss, simp_attrs),
            (selN, sel_thmss, simp_attrs),