don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Oct 02 15:53:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Oct 02 16:29:40 2013 +0200
@@ -53,7 +53,7 @@
   type gfp_sugar_thms =
     ((thm list * thm) list * Args.src list)
     * (thm list list * thm list list * Args.src list)
-    * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
+    * (thm list list * thm list list * Args.src list)
     * (thm list list * thm list list * Args.src list)
     * (thm list list list * thm list list list * Args.src list)
 
@@ -397,7 +397,7 @@
 type gfp_sugar_thms =
   ((thm list * thm) list * Args.src list)
   * (thm list list * thm list list * Args.src list)
-  * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
+  * (thm list list * thm list list * Args.src list)
   * (thm list list * thm list list * Args.src list)
   * (thm list list list * thm list list list * Args.src list);
 
@@ -908,7 +908,7 @@
     val fcoiterss' as [gunfolds, hcorecs] =
       map2 (fn (pfss, _) => map (lists_bmoc pfss)) (map fst coiters_args_types) coiterss';
 
-    val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) =
+    val (unfold_thmss, corec_thmss) =
       let
         fun mk_goal pfss c cps fcoiter n k ctr m cfs' =
           fold_rev (fold_rev Logic.all) ([c] :: pfss)
@@ -956,18 +956,8 @@
         val corec_thmss =
           map2 (map2 prove) corec_goalss corec_tacss
           |> map (map (unfold_thms lthy @{thms sum_case_if}));
-
-        val unfold_safesss = map2 (map2 (map2 (curry op =))) crgsss' crgsss;
-        val corec_safesss = map2 (map2 (map2 (curry op =))) cshsss' cshsss;
-
-        val filter_safesss =
-          map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
-            curry (op ~~));
-
-        val safe_unfold_thmss = filter_safesss unfold_safesss unfold_thmss;
-        val safe_corec_thmss = filter_safesss corec_safesss corec_thmss;
       in
-        (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss)
+        (unfold_thmss, corec_thmss)
       end;
 
     val (disc_unfold_iff_thmss, disc_corec_iff_thmss) =
@@ -1035,7 +1025,6 @@
   in
     ((coinduct_thms_pairs, coinduct_case_attrs),
      (unfold_thmss, corec_thmss, code_nitpick_simp_attrs),
-     (safe_unfold_thmss, safe_corec_thmss),
      (disc_unfold_thmss, disc_corec_thmss, []),
      (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
      (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
@@ -1464,7 +1453,6 @@
         val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
               coinduct_attrs),
              (unfold_thmss, corec_thmss, coiter_attrs),
-             (safe_unfold_thmss, safe_corec_thmss),
              (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
              (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
              (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) =
@@ -1477,21 +1465,14 @@
 
         val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
 
-        fun flat_coiter_thms coiters disc_coiters disc_coiter_iffs sel_coiters =
-          coiters @ disc_coiters @ disc_coiter_iffs @ sel_coiters;
+        val flat_coiter_thms = append oo append;
 
         val simp_thmss =
           map7 mk_simp_thms ctr_sugars
-            (map4 flat_coiter_thms safe_unfold_thmss disc_unfold_thmss disc_unfold_iff_thmss
-               sel_unfold_thmss)
-            (map4 flat_coiter_thms safe_corec_thmss disc_corec_thmss disc_corec_iff_thmss
-               sel_corec_thmss)
+            (map3 flat_coiter_thms disc_unfold_thmss disc_unfold_iff_thmss sel_unfold_thmss)
+            (map3 flat_coiter_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
             mapss rel_injects rel_distincts setss;
 
-        val anonymous_notes =
-          [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
-          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
-
         val common_notes =
           (if nn > 1 then
              [(coinductN, [coinduct_thm], coinduct_attrs),
@@ -1521,7 +1502,7 @@
           |> Generic_Target.theory_declaration;
       in
         lthy
-        |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
+        |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
           ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
           (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])

--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Oct 02 15:53:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Oct 02 16:29:40 2013 +0200
@@ -157,7 +157,7 @@
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
             ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
-          |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _,
+          |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
                   (disc_unfold_thmss, disc_corec_thmss, _), _,
                   (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
             (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Oct 02 15:53:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Oct 02 16:29:40 2013 +0200
@@ -918,20 +918,10 @@
         val ctr_thmss = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss
           (map #ctr_specs corec_specs);
 
-        val safess = map (map (not o exists_subterm (member (op =) (map SOME fun_names) o
-          try (fst o dest_Free)) o snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o
-          Logic.strip_imp_concl o drop_All o prop_of)) ctr_thmss;
-        val safe_ctr_thmss = map (map snd o filter fst o (op ~~)) (safess ~~ ctr_thmss);
-
-        val simp_thmss =
-          map3 (fn x => fn y => fn z => x @ y @ z) disc_thmss sel_thmss safe_ctr_thmss;
+        val simp_thmss = map2 append disc_thmss sel_thmss
 
         val common_name = mk_common_name fun_names;
 
-        val anonymous_notes =
-          [(flat safe_ctr_thmss, simp_attrs)]
-          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
-
         val notes =
           [(coinductN, map (if n2m then single else K []) coinduct_thms, []),
            (codeN, ctr_thmss(*FIXME*), code_nitpick_attrs),
@@ -953,7 +943,7 @@
           |> map (fn (thmN, thms, attrs) =>
             ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
       in
-        lthy |> Local_Theory.notes (anonymous_notes @ notes @ common_notes) |> snd
+        lthy |> Local_Theory.notes (notes @ common_notes) |> snd
       end;
 
     fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';