diff -r 5d1a7b688f6d -r f8900a5ad4a7 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Thu Oct 08 16:07:10 2020 +0200
+++ b/src/HOL/ATP.thy	Thu Oct 08 16:36:00 2020 +0200
@@ -15,7 +15,6 @@
 ML_file \<open>Tools/ATP/atp_problem.ML\<close>
 ML_file \<open>Tools/ATP/atp_proof.ML\<close>
 ML_file \<open>Tools/ATP/atp_proof_redirect.ML\<close>
-ML_file \<open>Tools/ATP/atp_satallax.ML\<close>
 
 
 subsection \<open>Higher-order reasoning helpers\<close>