src/HOL/Tools/inductive_realizer.ML
changeset 19510 29fc4e5a638c
parent 19473 d87a8838afa4
child 19617 7cb4b67d4b97
equal deleted inserted replaced
19509:351e1b1ea251 19510:29fc4e5a638c
   306       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
   306       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
   307 
   307 
   308     val thy1' = thy1 |>
   308     val thy1' = thy1 |>
   309       Theory.copy |>
   309       Theory.copy |>
   310       Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
   310       Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
   311       Theory.add_arities_i (map (fn s =>
   311       fold (fn s => AxClass.axiomatize_arity_i
   312         (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames) |>
   312         (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
   313         Extraction.add_typeof_eqns_i ty_eqs;
   313         Extraction.add_typeof_eqns_i ty_eqs;
   314     val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
   314     val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
   315       SOME (dt_of_intrs thy1' vs rs) else NONE) rss;
   315       SOME (dt_of_intrs thy1' vs rs) else NONE) rss;
   316 
   316 
   317     (** datatype representing computational content of inductive set **)
   317     (** datatype representing computational content of inductive set **)