src/HOL/Tools/inductive_set.ML
changeset 61162 61908914d191
parent 61144 5e94dfead1c2
child 61163 c94c65f35d01
equal deleted inserted replaced
61161:8fbab2f3433f 61162:61908914d191
   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))