equal
deleted
inserted
replaced
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 Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
250 |
250 |
251 val (alpha_info, lthy') = Inductive.add_inductive_i |
251 val (alpha_info, lthy') = Inductive.add_inductive_i |
252 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
252 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
253 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
253 coind = false, no_elim = false, no_ind = false, skip_mono = false} |
254 all_alpha_names [] all_alpha_intros [] lthy |
254 all_alpha_names [] all_alpha_intros [] lthy |
255 |
255 |
256 val all_alpha_trms_loc = #preds alpha_info; |
256 val all_alpha_trms_loc = #preds alpha_info; |
257 val alpha_raw_induct_loc = #raw_induct alpha_info; |
257 val alpha_raw_induct_loc = #raw_induct alpha_info; |
258 val alpha_intros_loc = #intrs alpha_info; |
258 val alpha_intros_loc = #intrs alpha_info; |