# HG changeset patch
# User blanchet
# Date 1389361177 -3600
# Node ID baa2baf29eff676f4da27ce0253d19112090eb71
# Parent  78de75e3e52a8d8df12065480357aee0e54feb09
use 'disc_iff' as simp rules whenever possible + clean up '= True', '= False', etc.

diff -r 78de75e3e52a -r baa2baf29eff src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
@@ -1254,6 +1254,8 @@
                   (the_single exhaust_thms) (the_single disc_thms) disc_thmss' (flat disc_excludess)
                 |> K |> Goal.prove_sorry lthy [] [] goal
                 |> Thm.close_derivation
+                |> fold (fn rule => perhaps (try (fn thm => thm RS rule)))
+                  @{thms eqTrueE eq_False[THEN iffD1] notnotD}
                 |> pair eqn_pos
                 |> single
             end;
@@ -1270,7 +1272,9 @@
         val code_thmss = map6 prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss'
           ctr_specss;
 
-        val simp_thmss = map2 append disc_thmss sel_thmss;
+        val disc_iff_or_disc_thmss =
+          map2 (fn [] => I | disc_iffs => K disc_iffs) disc_iff_thmss disc_thmss;
+        val simp_thmss = map2 append disc_iff_or_disc_thmss sel_thmss;
 
         val common_name = mk_common_name fun_names;