src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
changeset 72400 abfeed05c323
parent 69593 3dda49e08b9d
child 73939 9231ea46e041
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Oct 08 16:36:00 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Oct 08 17:02:56 2020 +0200
@@ -34,11 +34,11 @@
 open ATP_Proof
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
-open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer_Fact
 open Sledgehammer_Proof_Methods
 open Sledgehammer_Isar
+open Sledgehammer_ATP_Systems
 open Sledgehammer_Prover
 open Sledgehammer_Prover_ATP
 open Sledgehammer_Prover_SMT