changeset 3190 | 1b7c034c9e9e |
parent 3181 | ca162f0a7957 |
child 3201 | 3e6f4320669f |
--- 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) *}