--- a/Quot/quotient_info.ML	Wed Feb 10 20:35:54 2010 +0100
+++ b/Quot/quotient_info.ML	Wed Feb 10 21:39:40 2010 +0100
@@ -44,32 +44,6 @@
 end;
 
 
-functor Filtered_Named_Thms (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
 
@@ -262,10 +236,9 @@
 val equiv_rules_add = EquivRules.add
 
 (* respectfulness theorems *)
-structure RspRules = Filtered_Named_Thms
+structure RspRules = Named_Thms
   (val name = "quot_respect"
-   val description = "Respectfulness theorems."
-   val filter = I)
+   val description = "Respectfulness theorems.")
 
 val rsp_rules_get = RspRules.get