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, |
296 ({fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, rel_sels, |
297 rel_intros, rel_cases, set_thms, set_sels, set_intros, ...}, ...} : fp_sugar) = |
297 rel_intros, rel_cases, set_thms, set_sels, set_intros, set_cases, ...}, |
|
298 ...} : fp_sugar) = |
298 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, |
299 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, |
299 pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs, |
300 pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs, |
300 live_nesting_bnfs = live_nesting_bnfs, |
301 live_nesting_bnfs = live_nesting_bnfs, |
301 fp_ctr_sugar = |
302 fp_ctr_sugar = |
302 {ctrXs_Tss = ctrXs_Tss, |
303 {ctrXs_Tss = ctrXs_Tss, |
311 rel_sels = rel_sels, |
312 rel_sels = rel_sels, |
312 rel_intros = rel_intros, |
313 rel_intros = rel_intros, |
313 rel_cases = rel_cases, |
314 rel_cases = rel_cases, |
314 set_thms = set_thms, |
315 set_thms = set_thms, |
315 set_sels = set_sels, |
316 set_sels = set_sels, |
316 set_intros = set_intros}, |
317 set_intros = set_intros, |
|
318 set_cases = set_cases}, |
317 fp_co_induct_sugar = |
319 fp_co_induct_sugar = |
318 {co_rec = co_rec, |
320 {co_rec = co_rec, |
319 common_co_inducts = common_co_inducts, |
321 common_co_inducts = common_co_inducts, |
320 co_inducts = co_inducts, |
322 co_inducts = co_inducts, |
321 co_rec_def = co_rec_def, |
323 co_rec_def = co_rec_def, |