1.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Jun 25 14:54:45 2008 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Jun 25 17:38:32 2008 +0200
     1.3 @@ -291,7 +291,7 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -val _ = OuterSyntax.keywords ["permissive", "congs", "hints"];
     1.8 +val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
     1.9  
    1.10  val hints =
    1.11    P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;