# HG changeset patch
# User blanchet
# Date 1572013684 -7200
# Node ID 849311b454285fa3461a6ea50a3451f35a40bb87
# Parent  ccc771091a78294003995f8659d057e5e2e0b72d
compile

diff -r ccc771091a78 -r 849311b45428 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Fri Oct 25 16:27:27 2019 +0200
+++ b/src/HOL/ATP.thy	Fri Oct 25 16:28:04 2019 +0200
@@ -137,5 +137,6 @@
 ML_file \<open>Tools/monomorph.ML\<close>
 ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
 ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
+ML_file \<open>Tools/ATP/atp_systems.ML\<close>
 
 end
diff -r ccc771091a78 -r 849311b45428 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Fri Oct 25 16:27:27 2019 +0200
+++ b/src/HOL/Sledgehammer.thy	Fri Oct 25 16:28:04 2019 +0200
@@ -16,8 +16,6 @@
 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>
@@ -37,7 +35,4 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
 
-lemma "1 + 1 = 2"
-  sledgehammer [iprover, overlord, dont_minimize, dont_preplay]
-
 end