diff -r f8900a5ad4a7 -r abfeed05c323 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Oct 08 16:36:00 2020 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Oct 08 17:02:56 2020 +0200 @@ -29,10 +29,10 @@ open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct -open ATP_Systems open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar +open Sledgehammer_ATP_Systems open Sledgehammer_Prover (* Empty string means create files in Isabelle's temporary files directory. *)