src/HOL/Library/refute.ML

 
 
 (* 'refute' command *)
 
 val _ =
-  Outer_Syntax.command @{command_spec "refute"}
+  Outer_Syntax.command @{command_keyword refute}
     "try to find a model that refutes a given subgoal"
     (scan_parms -- Scan.optional Parse.nat 1 >>
       (fn (parms, i) =>
         Toplevel.unknown_proof o
         Toplevel.keep (fn state =>

 
 
 (* 'refute_params' command *)
 
 val _ =
-  Outer_Syntax.command @{command_spec "refute_params"}
+  Outer_Syntax.command @{command_keyword refute_params}
     "show/store default parameters for the 'refute' command"
     (scan_parms >> (fn parms =>
       Toplevel.theory (fn thy =>
         let
           val thy' = fold set_default_param parms thy;