486 coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono} |
486 coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono} |
487 cs' intros' monos' params1 cnames_syn' lthy; |
487 cs' intros' monos' params1 cnames_syn' lthy; |
488 |
488 |
489 (* define inductive sets using previously defined predicates *) |
489 (* define inductive sets using previously defined predicates *) |
490 val (defs, lthy2) = lthy1 |
490 val (defs, lthy2) = lthy1 |
491 |> Local_Theory.conceal (* FIXME ?? *) |
491 |> Local_Theory.concealed (* FIXME ?? *) |
492 |> fold_map Local_Theory.define |
492 |> fold_map Local_Theory.define |
493 (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []), |
493 (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []), |
494 fold_rev lambda params (HOLogic.Collect_const U $ |
494 fold_rev lambda params (HOLogic.Collect_const U $ |
495 HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) |
495 HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) |
496 (cnames_syn ~~ cs_info ~~ preds)) |
496 (cnames_syn ~~ cs_info ~~ preds)) |