--- a/Quot/quotient_info.ML	Tue Dec 08 11:17:56 2009 +0100
+++ b/Quot/quotient_info.ML	Tue Dec 08 11:20:01 2009 +0100
@@ -26,6 +26,7 @@
   val equiv_rules_get: Proof.context -> thm list
   val equiv_rules_add: attribute
   val rsp_rules_get: Proof.context -> thm list  
+  val id_simps_get: Proof.context -> thm list
   val quotient_rules_get: Proof.context -> thm list
   val quotient_rules_add: attribute
 end;
@@ -62,6 +63,10 @@
   val tyname = Sign.intern_type thy tystr
   val mapname = Sign.intern_const thy mapstr
   val relname = Sign.intern_const thy relstr
+
+  fun check s = (Const (s, dummyT) |> Syntax.check_term ctxt)
+        handle _ => error ("Constant " ^ s ^ " not declared.")
+  val _ =  map check [mapname, relname]
 in
   maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
 end
@@ -170,6 +175,9 @@
   OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
 
+(* FIXME/TODO: check the various lemmas conform *)
+(* with the required shape                      *)
+
 (* equivalence relation theorems *)
 structure EquivRules = Named_Thms
   (val name = "quotient_equiv"
@@ -185,6 +193,13 @@
 
 val rsp_rules_get = RspRules.get
 
+(* respectfulness theorems *)
+structure IdSimps = Named_Thms
+  (val name = "id_simps"
+   val description = "Identity simp rules for maps.")
+
+val id_simps_get = IdSimps.get
+
 (* quotient theorems *)
 structure QuotientRules = Named_Thms
   (val name = "quotient_thm"
@@ -197,6 +212,7 @@
 val _ = Context.>> (Context.map_theory 
     (EquivRules.setup #>
      RspRules.setup #>
+     IdSimps.setup #>
      QuotientRules.setup))
 
 end; (* structure *)