src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
changeset 53589 27c418b7b985
parent 53476 eb3865c3ee58
child 53590 b6dc5403cad1
equal deleted inserted replaced
53588:11a77e4aa98b 53589:27c418b7b985
   445         val discs = #discs (nth ctr_sugars index);
   445         val discs = #discs (nth ctr_sugars index);
   446         val selss = #selss (nth ctr_sugars index);
   446         val selss = #selss (nth ctr_sugars index);
   447         val p_ios = map SOME p_is @ [NONE];
   447         val p_ios = map SOME p_is @ [NONE];
   448         val collapses = #collapses (nth ctr_sugars index);
   448         val collapses = #collapses (nth ctr_sugars index);
   449         val corec_thms = co_rec_of (nth coiter_thmsss index);
   449         val corec_thms = co_rec_of (nth coiter_thmsss index);
   450         val disc_corecs = co_rec_of (nth disc_coitersss index);
   450         val disc_corecs = co_rec_of (nth disc_coitersss index)
       
   451           |> pad_list TrueI 1;
   451         val sel_corecss = co_rec_of (nth sel_coiterssss index);
   452         val sel_corecss = co_rec_of (nth sel_coiterssss index);
   452       in
   453       in
   453         map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms
   454         map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms
   454           disc_corecs sel_corecss
   455           disc_corecs sel_corecss
   455       end;
   456       end;