--- 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