diff -r df053507edba -r 37285ec4387d Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/quotient_def.ML	Sun Dec 20 00:53:35 2009 +0100
@@ -127,8 +127,9 @@
       (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
          OuterParse.term)
 
-val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
-  OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
+val _ = OuterSyntax.local_theory "quotient_definition" 
+	  "definition for constants over the quotient type"
+             OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
 
 end; (* structure *)