--- a/src/HOL/Tools/inductive_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/inductive_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -464,12 +464,11 @@
else standard (raw_induct RSN (2, rev_mp));
val thy'' = thy' |>
- PureThy.add_tthmss [(("intrs", Attribute.tthms_of intrs), [])] |>
- (if no_elim then I else PureThy.add_tthmss
- [(("elims", Attribute.tthms_of elims), [])]) |>
- (if no_ind then I else PureThy.add_tthms
- [(((if coind then "co" else "") ^ "induct",
- Attribute.tthm_of induct), [])]) |>
+ PureThy.add_thmss [(("intrs", intrs), [])] |>
+ (if no_elim then I else PureThy.add_thmss
+ [(("elims", elims), [])]) |>
+ (if no_ind then I else PureThy.add_thms
+ [(((if coind then "co" else "") ^ "induct", induct), [])]) |>
Theory.parent_path;
in (thy'',
@@ -517,7 +516,7 @@
val thy'' = thy' |>
(if coind then I
- else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) |>
+ else PureThy.add_thms [(("induct", induct), [])]) |>
Theory.parent_path
in (thy'',
@@ -600,8 +599,8 @@
val intr_ts'' = map subst intr_ts';
in add_inductive_i verbose false "" coind false false cs'' intr_ts''
- (Attribute.thms_of (PureThy.get_tthmss thy monos))
- (Attribute.thms_of (PureThy.get_tthmss thy con_defs)) thy
+ (PureThy.get_thmss thy monos)
+ (PureThy.get_thmss thy con_defs) thy
end;
end;