467 coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono} |
467 coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono} |
468 cs' intros' monos' params1 cnames_syn' lthy; |
468 cs' intros' monos' params1 cnames_syn' lthy; |
469 |
469 |
470 (* define inductive sets using previously defined predicates *) |
470 (* define inductive sets using previously defined predicates *) |
471 val (defs, lthy2) = lthy1 |
471 val (defs, lthy2) = lthy1 |
472 |> Proof_Context.concealed (* FIXME ?? *) |
|
473 |> fold_map Local_Theory.define |
472 |> fold_map Local_Theory.define |
474 (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []), |
473 (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []), |
475 fold_rev lambda params (HOLogic.Collect_const U $ |
474 fold_rev lambda params (HOLogic.Collect_const U $ |
476 HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) |
475 HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) |
477 (cnames_syn ~~ cs_info ~~ preds)) |
476 (cnames_syn ~~ cs_info ~~ preds)) |