# HG changeset patch
# User blanchet
# Date 1379613822 -7200
# Node ID c9068aade8597e24ea7733e8c01da4c52610184d
# Parent  c1911450b84a6833be4495a1f2881ce3938941a9
killed exceptional code that is anyway no longer needed, now that the 'simp' attribute has been taken away -- this solves issues in 'primcorec'

diff -r c1911450b84a -r c9068aade859 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Sep 19 20:03:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Sep 19 20:03:42 2013 +0200
@@ -996,10 +996,7 @@
         (map2 proves unfold_goalss unfold_tacss, map2 proves corec_goalss corec_tacss)
       end;
 
-    val is_triv_discI = is_triv_implies orf is_concl_refl;
-
-    fun mk_disc_coiter_thms coiters discIs =
-      map (op RS) (filter_out (is_triv_discI o snd) (coiters ~~ discIs));
+    fun mk_disc_coiter_thms coiters discIs = map (op RS) (coiters ~~ discIs);
 
     val disc_unfold_thmss = map2 mk_disc_coiter_thms unfold_thmss discIss;
     val disc_corec_thmss = map2 mk_disc_coiter_thms corec_thmss discIss;
diff -r c1911450b84a -r c9068aade859 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 20:03:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 20:03:42 2013 +0200
@@ -509,8 +509,7 @@
         val sel_thmss = #sel_thmss (nth ctr_sugars index);
         val collapses = #collapses (nth ctr_sugars index);
         val corec_thms = co_rec_of (nth coiter_thmsss index);
-        val disc_corecs = (case co_rec_of (nth disc_coitersss index) of [] => [TrueI]
-          | thms => thms);
+        val disc_corecs = co_rec_of (nth disc_coitersss index);
         val sel_corecss = co_rec_of (nth sel_coiterssss index);
       in
         map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses