diff -r f8900a5ad4a7 -r abfeed05c323 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Oct 08 16:36:00 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Oct 08 17:02:56 2020 +0200
@@ -81,13 +81,13 @@
 
 open ATP_Proof
 open ATP_Util
-open ATP_Systems
 open ATP_Problem
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 open Metis_Tactic
 open Sledgehammer_Fact
 open Sledgehammer_Proof_Methods
+open Sledgehammer_ATP_Systems
 
 (* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *)
 val SledgehammerN = "Sledgehammer"