diff -r 6cdba30c6d66 -r 91c374abde06 quotient_info.ML --- a/quotient_info.ML Thu Dec 03 14:02:05 2009 +0100 +++ b/quotient_info.ML Thu Dec 03 15:03:31 2009 +0100 @@ -164,14 +164,14 @@ (* respectfulness lemmas *) structure RspRules = Named_Thms - (val name = "quot_rsp" + (val name = "quotient_rsp" val description = "Respectfulness theorems.") val rsp_rules_get = RspRules.get (* quotient lemmas *) structure QuotientRules = Named_Thms - (val name = "quotient" + (val name = "quotient_thm" val description = "Quotient theorems.") val quotient_rules_get = QuotientRules.get