# HG changeset patch
# User blanchet
# Date 1379278943 -7200
# Node ID 44f15d386aae0ef9a71c792e6c0bde69f8bbbd3e
# Parent  eb8362530715e47dd5d978a3fcb8ad001e428347
added missing theorems to "simps" collection

diff -r eb8362530715 -r 44f15d386aae src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Sep 15 23:02:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Sep 15 23:02:23 2013 +0200
@@ -1479,13 +1479,15 @@
 
         val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
 
-        fun flat_coiter_thms coiters disc_coiters sel_coiters =
-          coiters @ disc_coiters @ sel_coiters;
+        fun flat_coiter_thms coiters disc_coiters disc_coiter_iffs sel_coiters =
+          coiters @ disc_coiters @ disc_coiter_iffs @ sel_coiters;
 
         val simp_thmss =
           mk_simp_thmss ctr_sugars
-            (map3 flat_coiter_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss)
-            (map3 flat_coiter_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
+            (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)
             mapss rel_injects rel_distincts setss;
 
         val anonymous_notes =