291 |
291 |
292 val phi = Proof_Context.export_morphism names_lthy no_defs_lthy; |
292 val phi = Proof_Context.export_morphism names_lthy no_defs_lthy; |
293 |
293 |
294 fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec |
294 fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec |
295 co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss |
295 co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss |
296 ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, ...}, |
296 ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...}, |
297 fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, |
297 fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, |
298 rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...}, |
298 rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...}, |
299 fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, |
299 fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, |
300 common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...}, |
300 common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...}, |
301 ...} : fp_sugar) = |
301 ...} : fp_sugar) = |
306 {ctrXs_Tss = ctrXs_Tss, |
306 {ctrXs_Tss = ctrXs_Tss, |
307 ctr_defs = ctr_defs, |
307 ctr_defs = ctr_defs, |
308 ctr_sugar = ctr_sugar, |
308 ctr_sugar = ctr_sugar, |
309 ctr_transfers = ctr_transfers, |
309 ctr_transfers = ctr_transfers, |
310 case_transfers = case_transfers, |
310 case_transfers = case_transfers, |
311 disc_transfers = disc_transfers}, |
311 disc_transfers = disc_transfers, |
|
312 sel_transfers = sel_transfers}, |
312 fp_bnf_sugar = |
313 fp_bnf_sugar = |
313 {map_thms = map_thms, |
314 {map_thms = map_thms, |
314 map_disc_iffs = map_disc_iffs, |
315 map_disc_iffs = map_disc_iffs, |
315 map_selss = map_selss, |
316 map_selss = map_selss, |
316 rel_injects = rel_injects, |
317 rel_injects = rel_injects, |