| changeset 27353 | 71c4dd53d4cb |
| parent 26988 | 742e26213212 |
| child 27727 | 2397e310b2cc |
--- a/src/HOL/Tools/recdef_package.ML Wed Jun 25 14:54:45 2008 +0200 +++ b/src/HOL/Tools/recdef_package.ML Wed Jun 25 17:38:32 2008 +0200 @@ -291,7 +291,7 @@ local structure P = OuterParse and K = OuterKeyword in -val _ = OuterSyntax.keywords ["permissive", "congs", "hints"]; +val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"]; val hints = P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;