239 |
239 |
240 val (alphas, lthy') = Inductive.add_inductive_i |
240 val (alphas, lthy') = Inductive.add_inductive_i |
241 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
241 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
242 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
242 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
243 all_alpha_names [] all_alpha_eqs [] lthy |
243 all_alpha_names [] all_alpha_eqs [] lthy |
244 in |
244 |
245 (alphas, lthy') |
245 val alpha_ts_loc = #preds alphas; |
246 end |
246 val alpha_induct_loc = #induct alphas; |
247 *} |
247 val alpha_intros_loc = #intrs alphas; |
248 |
248 val alpha_cases_loc = #elims alphas; |
249 end |
249 val morphism = ProofContext.export_morphism lthy' lthy; |
|
250 |
|
251 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc; |
|
252 val alpha_induct = Morphism.thm morphism alpha_induct_loc; |
|
253 val alpha_intros = Morphism.fact morphism alpha_intros_loc |
|
254 val alpha_cases = Morphism.fact morphism alpha_cases_loc |
|
255 in |
|
256 (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy') |
|
257 end |
|
258 *} |
|
259 |
|
260 end |