| changeset 17057 | 0934ac31985f |
| parent 16646 | 666774b0d1b0 |
| child 17261 | 193b84a70ca4 |
--- a/src/HOL/Tools/recdef_package.ML Tue Aug 16 13:42:23 2005 +0200 +++ b/src/HOL/Tools/recdef_package.ML Tue Aug 16 13:42:26 2005 +0200 @@ -338,7 +338,7 @@ (* outer syntax *) -local structure P = OuterParse and K = OuterSyntax.Keyword in +local structure P = OuterParse and K = OuterKeyword in val hints = P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;