299 live_nesting_bnfs = live_nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, |
299 live_nesting_bnfs = live_nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, |
300 ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps, |
300 ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps, |
301 common_co_inducts = common_co_inducts, co_inducts = co_inducts, |
301 common_co_inducts = common_co_inducts, co_inducts = co_inducts, |
302 co_rec_thms = co_rec_thms, co_rec_discs = co_rec_disc_thms, |
302 co_rec_thms = co_rec_thms, co_rec_discs = co_rec_disc_thms, |
303 co_rec_selss = co_rec_sel_thmss, rel_injects = rel_injects, |
303 co_rec_selss = co_rec_sel_thmss, rel_injects = rel_injects, |
304 rel_distincts = rel_distincts} |
304 rel_distincts = rel_distincts, fp_ctr_sugar = {}, fp_bnf_sugar = {}, |
|
305 fp_co_induct_sugar = {}} |
305 |> morph_fp_sugar phi; |
306 |> morph_fp_sugar phi; |
306 |
307 |
307 val target_fp_sugars = |
308 val target_fp_sugars = |
308 map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars |
309 map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars |
309 co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss co_rec_disc_thmss |
310 co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss co_rec_disc_thmss |