src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

     (case AList.lookup (op =) args proverK of
       SOME name => get_prover name
     | NONE => get_prover (default_prover_name ()))
   end
 
-type locality = ATP_Translate.locality
+type locality = ATP_Problem_Generate.locality
 
 (* hack *)
 fun reconstructor_from_msg args msg =
   (case AList.lookup (op =) args reconstructorK of
     SOME name => name

         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     fun failed failure =
       ({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
         preplay =
-          K (ATP_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis),
+          K (ATP_Proof_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis),
         message = K "", message_tail = ""}, ~1)
     val ({outcome, used_facts, run_time, preplay, message, message_tail}
          : Sledgehammer_Provers.prover_result,
         time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
       let

         if !reconstructor = "sledgehammer_tac" then
           sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_simple"
           ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
           ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
           ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
-          ORELSE' Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
+          ORELSE' Metis_Tactic.metis_tac [] ATP_Problem_Generate.combinatorsN
+            ctxt thms
         else if !reconstructor = "smt" then
           SMT_Solver.smt_tac ctxt thms
         else if full then
-          Metis_Tactic.metis_tac [ATP_Reconstruct.full_typesN]
-            ATP_Reconstruct.metis_default_lam_trans ctxt thms
+          Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN]
+            ATP_Proof_Reconstruct.metis_default_lam_trans ctxt thms
         else if String.isPrefix "metis (" (!reconstructor) then
           let
             val (type_encs, lam_trans) =
               !reconstructor
               |> Outer_Syntax.scan Position.start
               |> filter Token.is_proper |> tl
               |> Metis_Tactic.parse_metis_options |> fst
-              |>> the_default [ATP_Reconstruct.partial_typesN]
-              ||> the_default ATP_Reconstruct.metis_default_lam_trans
+              |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
+              ||> the_default ATP_Proof_Reconstruct.metis_default_lam_trans
           in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
         else if !reconstructor = "metis" then
-          Metis_Tactic.metis_tac [] ATP_Reconstruct.metis_default_lam_trans ctxt
+          Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.metis_default_lam_trans ctxt
             thms
         else
           K all_tac
       end
     fun apply_reconstructor named_thms =