diff -r 936718dede80 -r e771b8157fc7 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Apr 23 13:49:46 2020 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Apr 23 15:45:42 2020 +0200
@@ -16,6 +16,7 @@
 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
   by (erule contrapos_nn) (rule arg_cong)
 
+ML_file \<open>Tools/ATP/atp_systems.ML\<close>
 ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>