# HG changeset patch
# User blanchet
# Date 1379925926 -7200
# Node ID dfa1108368ad09a01abd108da935a9c856784430
# Parent  af7d1533a25b3a1c75343916a99bff8f63c40285
generate "simps" from "primcorec"

diff -r af7d1533a25b -r dfa1108368ad src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Sep 23 10:38:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Sep 23 10:45:26 2013 +0200
@@ -839,6 +839,10 @@
           map2 (map_filter (fn (safe, thm) => if safe then SOME thm else NONE) oo curry (op ~~))
             safess ctr_thmss;
 
+        fun mk_simp_thms disc_thms sel_thms ctr_thms = disc_thms @ sel_thms @ ctr_thms;
+
+        val simp_thmss = map3 mk_simp_thms disc_thmss sel_thmss safe_ctr_thmss;
+
         val anonymous_notes =
           [(flat safe_ctr_thmss, simp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
@@ -846,7 +850,8 @@
         val notes =
           [(ctrN, ctr_thmss, []),
            (discN, disc_thmss, simp_attrs),
-           (selN, sel_thmss, simp_attrs)]
+           (selN, sel_thmss, simp_attrs),
+           (simpsN, simp_thmss, [])]
           |> maps (fn (thmN, thmss, attrs) =>
             map2 (fn fun_name => fn thms =>
                 ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]))