--- a/quotient_info.ML	Sun Nov 29 02:51:42 2009 +0100
+++ b/quotient_info.ML	Sun Nov 29 03:59:18 2009 +0100
@@ -18,6 +18,8 @@
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic 
   val print_qconstinfo: Proof.context -> unit
+
+  val rsp_rules_get: Proof.context -> thm list  
 end;
 
 structure Quotient_Info: QUOTIENT_INFO =
@@ -111,7 +113,7 @@
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
 
 
-(* information about quotient constants *)
+(* info about quotient constants *)
 type qconsts_info = {qconst: term, rconst: term}
 
 structure QConstsData = Theory_Data
@@ -148,6 +150,15 @@
   OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
 
+(* respectfulness lemmas *)
+structure RspRules = Named_Thms
+  (val name = "quot_rsp"
+   val description = "Respectfulness theorems.")
+
+val rsp_rules_get = RspRules.get
+
+val _ = Context.>> (Context.map_theory RspRules.setup)
+
 end; (* structure *)
 
 open Quotient_Info