diff -r 070161f1996a -r a082e2d138ab quotient_info.ML
--- a/quotient_info.ML	Sun Dec 06 11:39:34 2009 +0100
+++ b/quotient_info.ML	Sun Dec 06 13:41:42 2009 +0100
@@ -23,6 +23,8 @@
   val qconsts_dest: theory -> qconsts_info list
   val print_qconstinfo: Proof.context -> unit
 
+  val equiv_rules_get: Proof.context -> thm list
+  val equiv_rules_add: attribute
   val rsp_rules_get: Proof.context -> thm list  
   val quotient_rules_get: Proof.context -> thm list
   val quotient_rules_add: attribute
@@ -168,24 +170,33 @@
   OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
 
-(* respectfulness lemmas *)
+(* equivalence relation theorems *)
+structure EquivRules = Named_Thms
+  (val name = "quotient_equiv"
+   val description = "Equivalence relation theorems.")
+
+val equiv_rules_get = EquivRules.get
+val equiv_rules_add = EquivRules.add
+
+(* respectfulness theorems *)
 structure RspRules = Named_Thms
   (val name = "quotient_rsp"
    val description = "Respectfulness theorems.")
 
 val rsp_rules_get = RspRules.get
 
-(* quotient lemmas *)
+(* quotient theorems *)
 structure QuotientRules = Named_Thms
   (val name = "quotient_thm"
    val description = "Quotient theorems.")
 
 val quotient_rules_get = QuotientRules.get
-val quotient_rules_add = Thm.declaration_attribute QuotientRules.add_thm
+val quotient_rules_add = QuotientRules.add
 
 (* setup of the theorem lists *)
 val _ = Context.>> (Context.map_theory 
-    (RspRules.setup #>
+    (EquivRules.setup #>
+     RspRules.setup #>
      QuotientRules.setup))
 
 end; (* structure *)