208 val constrs_info = all_dtyp_constrs_types descr sorts |
208 val constrs_info = all_dtyp_constrs_types descr sorts |
209 |
209 |
210 val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss |
210 val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss |
211 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info |
211 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info |
212 |
212 |
213 val all_alpha_names = map2 (fn s => fn ty => ((Binding.name s, ty), NoSyn)) |
213 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
214 (alpha_names @ alpha_bn_names) (alpha_tys @ alpha_bn_tys) |
214 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
215 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
215 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
216 |
216 |
217 val (alphas, lthy') = Inductive.add_inductive_i |
217 val (alphas, lthy') = Inductive.add_inductive_i |
218 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
218 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
219 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
219 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |