# HG changeset patch
# User blanchet
# Date 1379628522 -7200
# Node ID 9db52ae900093d4fa048a787cf2b51f2b637356e
# Parent  87585d506db4ec7870bbeadc3c0ed885ee25c932
setting the stage for safe constructor simp rules

diff -r 87585d506db4 -r 9db52ae90009 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 23:54:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Sep 20 00:08:42 2013 +0200
@@ -827,7 +827,7 @@
               |> single
           end;
 
-        (* TODO: please reorganize so that the list looks like elsewhere in the BNF code.
+        (* TODO: Reorganize so that the list looks like elsewhere in the BNF code.
            This is important because we continually add new theorems, change attributes, etc., and
            need to have a clear overview (and keep the documentation in sync). Also, it's confusing
            that some variables called '_thmss' are actually pairs. *)
@@ -839,14 +839,25 @@
           fun_names ~~ map4 (map ooo prove_sel) corec_specs disc_eqnss exclssss sel_eqnss
           |> `(map (fn (fun_name, thms) =>
             ((Binding.qualify true fun_name (@{binding sel}), simp_attrs), [(map snd thms, [])])));
+
+        val ctr_thmss = map5 (maps oooo prove_ctr) disc_thmss sel_thmss disc_eqnss sel_eqnss
+          (map #ctr_specs corec_specs);
+        val safess = map (map (K false)) ctr_thmss; (* FIXME: "true" for non-corecursive theorems *)
+        val safe_ctr_thmss =
+          map2 (map_filter (fn (safe, thm) => if safe then SOME thm else NONE) oo curry (op ~~))
+            safess ctr_thmss;
+
         val ctr_notes =
-          fun_names ~~ map5 (maps oooo prove_ctr) disc_thmss sel_thmss
-            disc_eqnss sel_eqnss (map #ctr_specs corec_specs)
+          fun_names ~~ ctr_thmss
           |> map (fn (fun_name, thms) =>
             ((Binding.qualify true fun_name (@{binding ctr}), []), [(thms, [])]));
+
+        val anonymous_notes =
+          [(flat safe_ctr_thmss, simp_attrs)]
+          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
       in
-        lthy |> snd o Local_Theory.notes
-          (filter (not o null o fst o the_single o snd) (disc_notes @ sel_notes @ ctr_notes))
+        lthy |> snd o Local_Theory.notes (anonymous_notes @
+          filter (not o null o fst o the_single o snd) (disc_notes @ sel_notes @ ctr_notes))
       end;
   in
     lthy'