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