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_bnf_sugar = {map_disc_iffs, rel_injects, rel_distincts, ...}, ...} : fp_sugar) = |
296 ({fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, ...}, ...} : fp_sugar) = |
297 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, |
297 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, |
298 pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs, |
298 pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs, |
299 live_nesting_bnfs = live_nesting_bnfs, |
299 live_nesting_bnfs = live_nesting_bnfs, |
300 fp_ctr_sugar = |
300 fp_ctr_sugar = |
301 {ctrXs_Tss = ctrXs_Tss, |
301 {ctrXs_Tss = ctrXs_Tss, |
302 ctr_defs = ctr_defs, |
302 ctr_defs = ctr_defs, |
303 ctr_sugar = ctr_sugar}, |
303 ctr_sugar = ctr_sugar}, |
304 fp_bnf_sugar = |
304 fp_bnf_sugar = |
305 {map_thms = map_thms, |
305 {map_thms = map_thms, |
306 map_disc_iffs = map_disc_iffs, |
306 map_disc_iffs = map_disc_iffs, |
|
307 map_sels = map_sels, |
307 rel_injects = rel_injects, |
308 rel_injects = rel_injects, |
308 rel_distincts = rel_distincts}, |
309 rel_distincts = rel_distincts}, |
309 fp_co_induct_sugar = |
310 fp_co_induct_sugar = |
310 {co_rec = co_rec, |
311 {co_rec = co_rec, |
311 common_co_inducts = common_co_inducts, |
312 common_co_inducts = common_co_inducts, |