equal
deleted
inserted
replaced
336 (recdef_wfN, wf_attr, "declaration of recdef wf rule")]]; |
336 (recdef_wfN, wf_attr, "declaration of recdef wf rule")]]; |
337 |
337 |
338 |
338 |
339 (* outer syntax *) |
339 (* outer syntax *) |
340 |
340 |
341 local structure P = OuterParse and K = OuterSyntax.Keyword in |
341 local structure P = OuterParse and K = OuterKeyword in |
342 |
342 |
343 val hints = |
343 val hints = |
344 P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src; |
344 P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src; |
345 |
345 |
346 val recdef_decl = |
346 val recdef_decl = |