1.1 --- a/src/HOL/Tools/record.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -2311,7 +2311,7 @@
     1.4  (* outer syntax *)
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
     1.8 +  Outer_Syntax.command @{command_spec "record"} "define extensible record"
     1.9      (Parse.type_args_constrained -- Parse.binding --
    1.10        (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
    1.11          Scan.repeat1 Parse.const_binding)