--- a/quotient_info.ML	Thu Dec 03 11:40:10 2009 +0100
+++ b/quotient_info.ML	Thu Dec 03 13:59:53 2009 +0100
@@ -21,6 +21,8 @@
   val print_qconstinfo: Proof.context -> unit
 
   val rsp_rules_get: Proof.context -> thm list  
+  val quotient_rules_get: Proof.context -> thm list
+  val quotient_rules_add: attribute
 end;
 
 structure Quotient_Info: QUOTIENT_INFO =
@@ -161,7 +163,18 @@
 
 val rsp_rules_get = RspRules.get
 
-val _ = Context.>> (Context.map_theory RspRules.setup)
+(* quotient lemmas *)
+structure QuotientRules = Named_Thms
+  (val name = "quotient"
+   val description = "Quotient theorems.")
+
+val quotient_rules_get = QuotientRules.get
+val quotient_rules_add = Thm.declaration_attribute QuotientRules.add_thm
+
+(* setup of the theorem lists *)
+val _ = Context.>> (Context.map_theory 
+    (RspRules.setup #>
+     QuotientRules.setup))
 
 end; (* structure *)