src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

 struct
 
 open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer
-open Sledgehammer_Fact_Minimizer
+open Sledgehammer_Fact_Minimize
 
 (** Sledgehammer commands **)
 
 fun add_to_relevance_override ns : relevance_override =
   {add = ns, del = [], only = false}

       let val i = the_default 1 opt_i in
         run_sledgehammer (get_params thy override_params) i relevance_override
                          (minimize_command override_params i) state
       end
     else if subcommand = minimizeN then
-      run_minimizer (get_params thy (map (apfst minimizize_raw_param_name)
-                                override_params))
-                    (the_default 1 opt_i) (#add relevance_override) state
+      run_minimize (get_params thy (map (apfst minimizize_raw_param_name)
+                               override_params))
+                   (the_default 1 opt_i) (#add relevance_override) state
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = available_atpsN then
       available_atps thy
     else if subcommand = running_atpsN then