src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

   in
     case result of
       SH_OK (time_isa, time_prover, names) =>
         let
           fun get_thms (name, stature) =
-            try (Sledgehammer_Reconstruct.thms_of_name (Proof.context_of st))
+            try (Sledgehammer_Util.thms_of_name (Proof.context_of st))
               name
             |> Option.map (pair (name, stature))
         in
           change_data id inc_sh_success;
           if trivial then () else change_data id inc_sh_nontriv_success;