diff -r e3cdbd929a24 -r d9db67970c73 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 12 13:54:51 1999 +0100
@@ -402,7 +402,7 @@
 
     val thy11 = thy10 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
+      PureThy.add_thmss [(("simps", simps), [])] |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       Theory.parent_path;
 
@@ -459,7 +459,7 @@
 
     val thy11 = thy10 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
+      PureThy.add_thmss [(("simps", simps), [])] |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       Theory.parent_path;
 
@@ -550,7 +550,7 @@
 
     val thy9 = thy8 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |>
+      PureThy.add_thmss [(("simps", simps), [])] |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       Theory.parent_path;
 
@@ -571,8 +571,7 @@
       simps = simps})
   end;
 
-val rep_datatype = gen_rep_datatype
-  (fn thy => Attribute.thms_of o PureThy.get_tthmss thy) get_thm;
+val rep_datatype = gen_rep_datatype (fn thy => PureThy.get_thmss thy) get_thm;
 val rep_datatype_i = gen_rep_datatype (K I) (K I);
 
 (******************************** add datatype ********************************)