# HG changeset patch # User haftmann # Date 1170255916 -3600 # Node ID bb07dd6cb1b95654b9c6794aa5ba7876c895e072 # Parent 8a8aa6114a893d03dbf770abf86440d21d56f774 clarified command annotation diff -r 8a8aa6114a89 -r bb07dd6cb1b9 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Wed Jan 31 16:05:14 2007 +0100 +++ b/src/Pure/Tools/class_package.ML Wed Jan 31 16:05:16 2007 +0100 @@ -574,7 +574,7 @@ >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort)); val classP = - OuterSyntax.command classK "define operational type class" K.thy_decl ( + OuterSyntax.command classK "define type class" K.thy_decl ( P.name --| P.$$$ "=" -- ( class_subP --| P.$$$ "+" -- class_bodyP