diff -r 526fad251a8e -r 0d059450a3fa Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Tue Feb 23 11:56:47 2010 +0100
+++ b/Quot/quotient_info.ML	Tue Feb 23 12:49:45 2010 +0100
@@ -37,7 +37,9 @@
   val equiv_rules_get: Proof.context -> thm list
   val equiv_rules_add: attribute
   val rsp_rules_get: Proof.context -> thm list
+  val rsp_rules_add: attribute
   val prs_rules_get: Proof.context -> thm list
+  val prs_rules_add: attribute
   val id_simps_get: Proof.context -> thm list
   val quotient_rules_get: Proof.context -> thm list
   val quotient_rules_add: attribute
@@ -241,6 +243,7 @@
    val description = "Respectfulness theorems.")
 
 val rsp_rules_get = RspRules.get
+val rsp_rules_add = RspRules.add
 
 (* preservation theorems *)
 structure PrsRules = Named_Thms
@@ -248,6 +251,7 @@
    val description = "Preservation theorems.")
 
 val prs_rules_get = PrsRules.get
+val prs_rules_add = PrsRules.add
 
 (* id simplification theorems *)
 structure IdSimps = Named_Thms