# HG changeset patch
# User berghofe
# Date 1133739487 -3600
# Node ID 58de95a16d3c69437eff29a1d732398c32658836
# Parent  b5d7649f8acac8bd4f8fda561f90b986579f1c34
Added store_thmss_atts to signature again.

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