changeset 59936 | b8ffc3dc9e24 |
parent 59859 | f9d1442c70f3 |
child 60326 | 68699e576d51 |
--- a/src/HOL/Tools/record.ML Mon Apr 06 16:30:44 2015 +0200 +++ b/src/HOL/Tools/record.ML Mon Apr 06 17:06:48 2015 +0200 @@ -2329,7 +2329,7 @@ (* outer syntax *) val _ = - Outer_Syntax.command @{command_spec "record"} "define extensible record" + Outer_Syntax.command @{command_keyword record} "define extensible record" (Parse.type_args_constrained -- Parse.binding -- (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) -- Scan.repeat1 Parse.const_binding)