src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

 
 val sledgehammerN = "sledgehammer"
 val sledgehammer_paramsN = "sledgehammer_params"
 
 val runN = "run"
-val minimizeN = "minimize"
+val minN = "min"
 val messagesN = "messages"
 val supported_proversN = "supported_provers"
 val running_proversN = "running_provers"
 val kill_proversN = "kill_provers"
 val refresh_tptpN = "refresh_tptp"

   member (op =) params_for_minimize o fst o unalias_raw_param
 fun string_for_raw_param (key, values) =
   key ^ (case implode_param values of "" => "" | value => " = " ^ value)
 
 fun minimize_command override_params i prover_name fact_names =
-  sledgehammerN ^ " " ^ minimizeN ^ " [prover = " ^ prover_name ^
+  sledgehammerN ^ " " ^ minN ^ " [prover = " ^ prover_name ^
   (override_params |> filter is_raw_param_relevant_for_minimize
                    |> implode o map (prefix ", " o string_for_raw_param)) ^
   "] (" ^ space_implode " " fact_names ^ ")" ^
   (if i = 1 then "" else " " ^ string_of_int i)
 

         run_sledgehammer (get_params false ctxt override_params) false i
                          relevance_override (minimize_command override_params i)
                          state
         |> K ()
       end
-    else if subcommand = minimizeN then
+    else if subcommand = minN then
       run_minimize (get_params false ctxt override_params) (the_default 1 opt_i)
                    (#add relevance_override) state
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = supported_proversN then