| changeset 27353 | 71c4dd53d4cb |
| parent 27352 | 8adeff7fd4bc |
| child 27449 | 4880da911af0 |
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Jun 25 14:54:45 2008 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Jun 25 17:38:32 2008 +0200 @@ -668,7 +668,7 @@ local structure P = OuterParse and K = OuterKeyword in -val _ = OuterSyntax.keywords ["avoids"]; +val _ = OuterKeyword.keyword "avoids"; val _ = OuterSyntax.command "nominal_inductive"