--- a/src/ZF/Tools/datatype_package.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/ZF/Tools/datatype_package.ML Tue Jan 12 13:54:51 1999 +0100
@@ -245,7 +245,7 @@
if need_recursor then
thy |> Theory.add_consts_i
[(recursor_base_name, recursor_typ, NoSyn)]
- |> PureThy.add_defs_i [Attribute.none recursor_def]
+ |> PureThy.add_defs_i [Thm.no_attributes recursor_def]
else thy;
val thy0 = thy_path
@@ -253,7 +253,7 @@
((case_base_name, case_typ, NoSyn) ::
map #1 (flat con_ty_lists))
|> PureThy.add_defs_i
- (map Attribute.none
+ (map Thm.no_attributes
(case_def ::
flat (ListPair.map mk_con_defs
(1 upto npart, con_ty_lists))))
@@ -392,8 +392,7 @@
in
(*Updating theory components: simprules and datatype info*)
(thy1 |> Theory.add_path big_rec_base_name
- |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps),
- [Simplifier.simp_add_global])]
+ |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
|> DatatypesData.put
(Symtab.update
((big_rec_name, dt_info), DatatypesData.get thy1))