--- a/Quot/quotient_info.ML	Sat Dec 26 23:20:46 2009 +0100
+++ b/Quot/quotient_info.ML	Sun Dec 27 23:33:10 2009 +0100
@@ -32,6 +32,34 @@
   val quotient_rules_add: attribute
 end;
 
+functor Named_Thms_Ext (val name: string val description: string val filter: thm -> thm): NAMED_THMS =
+struct
+
+structure Data = Generic_Data
+(
+  type T = thm Item_Net.T;
+  val empty = Thm.full_rules;
+  val extend = I;
+  val merge = Item_Net.merge;
+);
+
+val content = Item_Net.content o Data.get;
+val get = content o Context.Proof;
+
+val add_thm = Data.map o Item_Net.update o filter;
+val del_thm = Data.map o Item_Net.remove;
+
+val add = Thm.declaration_attribute add_thm;
+val del = Thm.declaration_attribute del_thm;
+
+val setup =
+  Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
+  PureThy.add_thms_dynamic (Binding.name name, content);
+
+end;
+
+
+
 structure Quotient_Info: QUOTIENT_INFO =
 struct
 
@@ -216,9 +244,10 @@
 val equiv_rules_add = EquivRules.add
 
 (* respectfulness theorems *)
-structure RspRules = Named_Thms
+structure RspRules = Named_Thms_Ext
   (val name = "quot_respect"
-   val description = "Respectfulness theorems.")
+   val description = "Respectfulness theorems."
+   val filter = fn x => x)
 
 val rsp_rules_get = RspRules.get