244 val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss |
244 val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss |
245 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_cns_info bclausesss) bn_info |
245 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_cns_info bclausesss) bn_info |
246 |
246 |
247 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
247 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
248 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
248 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
249 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
249 val all_alpha_intros = map (pair Binding.empty_atts) (flat alpha_intros @ flat alpha_bn_intros) |
250 |
250 |
251 val (alpha_info, lthy') = lthy |
251 val (alpha_info, lthy') = lthy |
252 |> Inductive.add_inductive_i |
252 |> Inductive.add_inductive_i |
253 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
253 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
254 coind = false, no_elim = false, no_ind = false, skip_mono = false} |
254 coind = false, no_elim = false, no_ind = false, skip_mono = false} |
284 alpha_bn_names = alpha_bn_names, |
284 alpha_bn_names = alpha_bn_names, |
285 alpha_bn_trms = alpha_bn_trms, |
285 alpha_bn_trms = alpha_bn_trms, |
286 alpha_bn_tys = alpha_bn_tys, |
286 alpha_bn_tys = alpha_bn_tys, |
287 alpha_intros = alpha_intros, |
287 alpha_intros = alpha_intros, |
288 alpha_cases = alpha_cases, |
288 alpha_cases = alpha_cases, |
289 alpha_raw_induct = alpha_raw_induct}, Local_Theory.restore lthy') |
289 alpha_raw_induct = alpha_raw_induct}, Local_Theory.reset lthy') (* FIXME disrupts context *) |
290 end |
290 end |
291 |
291 |
292 |
292 |
293 (** induction proofs **) |
293 (** induction proofs **) |
294 |
294 |