src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

     (case AList.lookup (op =) args proverK of
       SOME name => get_prover name
     | NONE => get_prover (default_atp_name ()))
   end
 
-type locality = Sledgehammer_Fact_Filter.locality
+type locality = Sledgehammer_Filter.locality
 
 local
 
 datatype sh_result =
   SH_OK of int * int * (string * locality) list |

     val (msg, result) = run_sh prover hard_timeout timeout dir st
   in
     case result of
       SH_OK (time_isa, time_atp, names) =>
         let
-          fun get_thms (name, Sledgehammer_Fact_Filter.Chained) = NONE
+          fun get_thms (name, Sledgehammer_Filter.Chained) = NONE
             | get_thms (name, loc) =
               SOME ((name, loc), thms_of_name (Proof.context_of st) name)
         in
           change_data id inc_sh_success;
           change_data id (inc_sh_lemmas (length names));

       |> Option.map (fst o read_int o explode)
       |> the_default 5
     val params = Sledgehammer_Isar.default_params thy
       [("atps", prover_name), ("timeout", Int.toString timeout ^ " s")]
     val minimize =
-      Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st)
+      Sledgehammer_Minimize.minimize_theorems params 1 (subgoal_count st)
     val _ = log separator
   in
     case minimize st (these (!named_thms)) of
       (SOME named_thms', msg) =>
         (change_data id inc_min_succs;