--- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Jan 12 13:54:51 1999 +0100
@@ -275,7 +275,7 @@
in
(thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
- PureThy.add_tthmss [(("recs", Attribute.tthms_of rec_thms), [])] |>
+ PureThy.add_thmss [(("recs", rec_thms), [])] |>
Theory.parent_path,
reccomb_names, rec_thms)
end;
@@ -518,7 +518,7 @@
in
(thy' |> Theory.add_path big_name |>
- PureThy.add_tthmss [(("size", Attribute.tthms_of size_thms), [])] |>
+ PureThy.add_thmss [(("size", size_thms), [])] |>
Theory.parent_path,
size_thms)
end;