changeset 444 | 3ca9d49fd662 |
parent 435 | ca5356bd315a |
child 454 | 0d19ab250cc9 |
--- a/src/ZF/intr_elim.ML Wed Jun 29 12:13:03 1994 +0200 +++ b/src/ZF/intr_elim.ML Fri Jul 01 11:03:42 1994 +0200 @@ -207,8 +207,10 @@ | _ => rec_tms ~~ (*define the sets as Parts*) map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); -val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive") - ([], [], [], [], [], [], None) axpairs; +val thy = + Ind.thy + |> add_axioms axpairs + |> add_thyname (big_rec_name ^ "_Inductive"); val defs = map (get_axiom thy o #1) axpairs;