src/HOL/Sledgehammer.thy

   ("Tools/Sledgehammer/meson_tactic.ML")
   ("Tools/Sledgehammer/metis_clauses.ML")
   ("Tools/Sledgehammer/metis_tactics.ML")
   ("Tools/Sledgehammer/sledgehammer_util.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
+  ("Tools/Sledgehammer/sledgehammer_translate.ML")
   ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
   ("Tools/Sledgehammer/sledgehammer.ML")
-  ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
+  ("Tools/Sledgehammer/sledgehammer_fact_minimize.ML")
   ("Tools/Sledgehammer/sledgehammer_isar.ML")
 begin
 
 definition skolem_id :: "'a \<Rightarrow> 'a" where
 [no_atp]: "skolem_id = (\<lambda>x. x)"

 use "Tools/Sledgehammer/metis_clauses.ML"
 use "Tools/Sledgehammer/metis_tactics.ML"
 
 use "Tools/Sledgehammer/sledgehammer_util.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
+use "Tools/Sledgehammer/sledgehammer_translate.ML"
 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
 use "Tools/Sledgehammer/sledgehammer.ML"
 setup Sledgehammer.setup
-use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
+use "Tools/Sledgehammer/sledgehammer_fact_minimize.ML"
 use "Tools/Sledgehammer/sledgehammer_isar.ML"
 setup Metis_Tactics.setup
 
 end