equal
deleted
inserted
replaced
245 |
245 |
246 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
246 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
247 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
247 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
248 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
248 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
249 |
249 |
250 val _ = tracing ("alpha in def\n" ^ cat_lines (map (@{make_string} o fst o #1) all_alpha_names)) |
|
251 |
|
252 val (alphas, lthy') = Inductive.add_inductive_i |
250 val (alphas, lthy') = Inductive.add_inductive_i |
253 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
251 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
254 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
252 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
255 all_alpha_names [] all_alpha_intros [] lthy |
253 all_alpha_names [] all_alpha_intros [] lthy |
256 |
254 |