author | haftmann |
Wed, 31 Jan 2007 16:05:16 +0100 | |
changeset 22222 | bb07dd6cb1b9 |
parent 22221 | 8a8aa6114a89 |
child 22223 | 69d4b98f4c47 |
--- 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