# HG changeset patch
# User blanchet
# Date 1393955837 -3600
# Node ID 461a75d0032347c3d56e88ff0aed3056786bf8c7
# Parent  39cc8409373f18c992e7caf4f2ea6eb71dc2d479
register relator equations as spec rules only for datatypes -- for codatatypes they underspecify the function and are therefore dangerous (e.g. to Nitpick)

diff -r 39cc8409373f -r 461a75d00323 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 04 18:57:17 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 04 18:57:17 2014 +0100
@@ -1267,7 +1267,8 @@
               (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar),
                lthy
                |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms)
-               |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms)
+               |> fp = Least_FP
+                 ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms)
                |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set_thms)
                |> Local_Theory.notes (anonymous_notes @ notes)
                |> snd)