diff -r eed5d55ea9a6 -r 6b3be083229c quotient_info.ML --- a/quotient_info.ML Fri Dec 04 09:08:51 2009 +0100 +++ b/quotient_info.ML Fri Dec 04 09:25:27 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