# HG changeset patch
# User blanchet
# Date 1379026544 -7200
# Node ID b6dc5403cad1188effc89c327c15b23c32151836
# Parent  27c418b7b98515a699ed437ad2068f3c1da5c94c
beware of multi-constructor datatypes (cf. 27c418b7b985)

diff -r 27c418b7b985 -r b6dc5403cad1 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Sep 13 00:39:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Sep 13 00:55:44 2013 +0200
@@ -447,8 +447,8 @@
         val p_ios = map SOME p_is @ [NONE];
         val collapses = #collapses (nth ctr_sugars index);
         val corec_thms = co_rec_of (nth coiter_thmsss index);
-        val disc_corecs = co_rec_of (nth disc_coitersss index)
-          |> pad_list TrueI 1;
+        val disc_corecs = (case co_rec_of (nth disc_coitersss index) of [] => [TrueI]
+          | thms => thms);
         val sel_corecss = co_rec_of (nth sel_coiterssss index);
       in
         map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms