src/HOL/Decision_Procs/approximation.ML

 
 val opt_modes =
   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
 
 val _ =
-  Outer_Syntax.command @{command_spec "approximate"} "print approximation of term"
+  Outer_Syntax.command @{command_keyword approximate} "print approximation of term"
     (opt_modes -- Parse.term
       >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
 
 fun approximation_tac prec splitting taylor ctxt i =
   REPEAT (FIRST' [etac @{thm intervalE},