# HG changeset patch
# User blanchet
# Date 1379025564 -7200
# Node ID 27c418b7b98515a699ed437ad2068f3c1da5c94c
# Parent  11a77e4aa98b8fff993c01c5c490bcdee3a1df9f
beware of single-constructor datatypes, with no discriminators

diff -r 11a77e4aa98b -r 27c418b7b985 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 12 23:43:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Sep 13 00:39:24 2013 +0200
@@ -447,7 +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);
+        val disc_corecs = co_rec_of (nth disc_coitersss index)
+          |> pad_list TrueI 1;
         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