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