src/Pure/Tools/thm_deps.ML

     Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []
     |> Graph_Display.display_graph
   end;
 
 val _ =
-  Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
+  Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
     (Parse.xthms1 >> (fn args =>
       Toplevel.unknown_theory o Toplevel.keep (fn state =>
         thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
 
 

              else ((a, th) :: thms, Inttab.update (grp, ()) seen_groups))
       else q) new_thms ([], Inttab.empty);
   in rev thms' end;
 
 val _ =
-  Outer_Syntax.command @{command_spec "unused_thms"} "find unused theorems"
+  Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
     (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
        Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
         Toplevel.keep (fn state =>
           let
             val thy = Toplevel.theory_of state;