diff -r 513074557e06 -r 16279c4c7a33 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Fri Mar 19 15:07:44 2010 +0100
+++ b/src/HOL/Sledgehammer.thy	Fri Mar 19 15:33:18 2010 +0100
@@ -101,29 +101,10 @@
 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
 setup Sledgehammer_Proof_Reconstruct.setup
 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
-
+use "Tools/ATP_Manager/atp_manager.ML"
 use "Tools/ATP_Manager/atp_wrapper.ML"
 setup ATP_Wrapper.setup
-use "Tools/ATP_Manager/atp_manager.ML"
 use "Tools/ATP_Manager/atp_minimal.ML"
-
-text {* basic provers *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
-
-text {* provers with stuctured output *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
-
-text {* on some problems better results *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
-
-text {* remote provers via SystemOnTPTP *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
-setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
-
 use "Tools/Sledgehammer/sledgehammer_isar.ML"