| changeset 56201 | dd2df97b379b |
| parent 56032 | b034b9f0fa2a |
| child 56249 | 0fda98dd2c93 |
--- a/src/HOL/Tools/recdef.ML Tue Mar 18 11:13:38 2014 +0100 +++ b/src/HOL/Tools/recdef.ML Tue Mar 18 11:27:09 2014 +0100 @@ -290,7 +290,7 @@ val hints = @{keyword "("} |-- - Parse.!!! (Parse.position @{keyword "hints"} -- Args.parse --| @{keyword ")"}) + Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"}) >> uncurry Args.src; val recdef_decl =