equal
deleted
inserted
replaced
204 (alpha_names @ alpha_bn_names) (alpha_types @ alpha_bn_types) |
204 (alpha_names @ alpha_bn_names) (alpha_types @ alpha_bn_types) |
205 val all_alpha_eqs = map (pair Attrib.empty_binding) (flat alpha_eqs @ flat alpha_bn_eqs) |
205 val all_alpha_eqs = map (pair Attrib.empty_binding) (flat alpha_eqs @ flat alpha_bn_eqs) |
206 |
206 |
207 val (alphas, lthy') = Inductive.add_inductive_i |
207 val (alphas, lthy') = Inductive.add_inductive_i |
208 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
208 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
209 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
209 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
210 all_alpha_names [] all_alpha_eqs [] lthy |
210 all_alpha_names [] all_alpha_eqs [] lthy |
211 |
211 |
212 val alpha_ts_loc = #preds alphas; |
212 val alpha_ts_loc = #preds alphas; |
213 val alpha_induct_loc = #raw_induct alphas; |
213 val alpha_induct_loc = #raw_induct alphas; |
214 val alpha_intros_loc = #intrs alphas; |
214 val alpha_intros_loc = #intrs alphas; |