diff -r e3cdbd929a24 -r d9db67970c73 src/ZF/Tools/datatype_package.ML
--- 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))