| changeset 61814 | 1ca1142e1711 |
| parent 61466 | 9a468c3a1fa1 |
| child 62058 | 1cfd5d604937 |
--- a/src/HOL/Library/old_recdef.ML Wed Dec 09 16:22:29 2015 +0100 +++ b/src/HOL/Library/old_recdef.ML Wed Dec 09 16:36:26 2015 +0100 @@ -2873,8 +2873,7 @@ val hints = @{keyword "("} |-- - Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"}) - >> uncurry Token.src; + Parse.!!! ((Parse.token @{keyword "hints"} ::: Parse.args) --| @{keyword ")"}); val recdef_decl = Scan.optional