155 sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) = |
155 sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) = |
156 if fp = Least_FP then |
156 if fp = Least_FP then |
157 derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct |
157 derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct |
158 xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss |
158 xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss |
159 co_iterss co_iter_defss lthy |
159 co_iterss co_iter_defss lthy |
160 |> `(fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) => |
160 |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) => |
161 ([induct], fold_thmss, rec_thmss, [], [], [], [])) |
161 ([induct], fold_thmss, rec_thmss, [], [], [], [])) |
162 ||> (fn info => (SOME info, NONE)) |
162 ||> (fn info => (SOME info, NONE)) |
163 else |
163 else |
164 derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct |
164 derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct |
165 dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss |
165 dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss |