# HG changeset patch
# User blanchet
# Date 1379671488 -7200
# Node ID a8253329ebe9bd5e1b99585d80fb5727277b2718
# Parent  bd038e48526dfb3d0ab0f33f955a31bb993cd467
took out spurious attributes (no need for several code equations / simps for thesame constants)

diff -r bd038e48526d -r a8253329ebe9 src/HOL/BNF/Tools/bnf_lfp_compat.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Fri Sep 20 11:44:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Fri Sep 20 12:04:48 2013 +0200
@@ -131,8 +131,7 @@
     val all_notes =
       (case lfp_sugar_thms of
         NONE => []
-      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs),
-              (rec_thmss, rec_attrs)) =>
+      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, _), (rec_thmss, _)) =>
         let
           val common_notes =
             (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
@@ -141,9 +140,9 @@
               ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
 
           val notes =
-            [(foldN, fold_thmss, fold_attrs),
+            [(foldN, fold_thmss, []),
              (inductN, map single induct_thms, induct_attrs),
-             (recN, rec_thmss, rec_attrs)]
+             (recN, rec_thmss, [])]
             |> filter_out (null o #2)
             |> maps (fn (thmN, thmss, attrs) =>
               if forall null thmss then