# HG changeset patch
# User blanchet
# Date 1444158284 -7200
# Node ID 2ebdd603cd71040e454d511a8dfa63f08717d230
# Parent  a696414fa3a18e93760ce3721d5660c3b33e96c9
avoid unsound 'nitpick_simp' attribute on nonterminating, nonproductive equations

diff -r a696414fa3a1 -r 2ebdd603cd71 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 06 19:35:33 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 06 21:04:44 2015 +0200
@@ -1102,7 +1102,7 @@
            (rel_injectN, rel_inject_thms, K simp_attrs),
            (rel_introsN, rel_intro_thms, K []),
            (rel_selN, rel_sel_thms, K []),
-           (setN, set_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
+           (setN, set_thms, K (code_attrs @ case_fp fp nitpicksimp_attrs [] @ simp_attrs)),
            (set_casesN, set_cases_thms, nth set_cases_attrss),
            (set_introsN, set_intros_thms, K []),
            (set_selN, set_sel_thms, K [])]