diff -r b5d7649f8aca -r 58de95a16d3c src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Sun Dec 04 12:40:39 2005 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Mon Dec 05 00:38:07 2005 +0100
@@ -15,6 +15,8 @@
   val add_path : bool -> string -> theory -> theory
   val parent_path : bool -> theory -> theory
 
+  val store_thmss_atts : string -> string list -> theory attribute list list -> thm list list
+    -> theory -> thm list list * theory
   val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
   val store_thms_atts : string -> string list -> theory attribute list list -> thm list
     -> theory -> thm list * theory