diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Mon Apr 06 17:06:48 2015 +0200
@@ -198,7 +198,7 @@
 val opt_overloaded = Parse.opt_keyword "overloaded"
 
 val _ =
-  Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
+  Outer_Syntax.command @{command_keyword specification} "define constants by specification"
     (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
       Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
       >> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props)))