src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     fun failed failure =
       ({outcome = SOME failure, used_facts = [], used_from = [],
         run_time = Time.zeroTime,
-        preplay = Lazy.value (Sledgehammer_Reconstructor.Metis_Method (NONE, NONE),
-          Sledgehammer_Reconstructor.Play_Failed),
+        preplay = Lazy.value (Sledgehammer_Proof_Methods.Metis_Method (NONE, NONE),
+          Sledgehammer_Proof_Methods.Play_Failed),
         message = K "", message_tail = ""}, ~1)
     val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
          : Sledgehammer_Prover.prover_result,
          time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
       let