diff -r e46d4ee64221 -r 1b7c034c9e9e Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Tue Jun 12 14:22:58 2012 +0100 +++ b/Nominal/Nominal2.thy Mon Jun 18 14:50:02 2012 +0100 @@ -748,7 +748,7 @@ end (* Command Keyword *) -val _ = Outer_Syntax.local_theory ("nominal_datatype", Keyword.thy_decl) +val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"} "declaration of nominal datatypes" (main_parser >> nominal_datatype2_cmd) *}