144 mk_ctr Ts ctr0 |> (fn Const (s, T) => (s, map2 mk_dtyp kkss (binder_types T))); |
144 mk_ctr Ts ctr0 |> (fn Const (s, T) => (s, map2 mk_dtyp kkss (binder_types T))); |
145 fun mk_typ_descr kksss ((Type (T_name, Ts), kk) :: parents) ctrs0 = |
145 fun mk_typ_descr kksss ((Type (T_name, Ts), kk) :: parents) ctrs0 = |
146 (kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0)); |
146 (kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0)); |
147 |
147 |
148 val descr = map3 mk_typ_descr kkssss Tparentss ctrss0; |
148 val descr = map3 mk_typ_descr kkssss Tparentss ctrss0; |
149 val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars; |
149 val recs = map (fst o dest_Const o #co_rec) fp_sugars; |
150 val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars; |
150 val rec_thms = maps #co_rec_thms fp_sugars; |
151 |
151 |
152 fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects, |
152 fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects, |
153 distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) = |
153 distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) = |
154 (T_name0, |
154 (T_name0, |
155 {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct, |
155 {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct, |