factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ATP.thy	Tue Oct 05 11:10:37 2010 +0200
@@ -0,0 +1,17 @@
+(*  Title:      HOL/ATP.thy
+    Author:     Fabian Immler, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+*)
+
+header {* Sledgehammer: Isabelle--ATP Linkup *}
+
+theory ATP
+imports Plain
+uses "Tools/ATP/atp_problem.ML"
+     "Tools/ATP/atp_proof.ML"
+     "Tools/ATP/atp_systems.ML"
+begin
+
+setup ATP_Systems.setup
+
+end

--- a/src/HOL/IsaMakefile	Tue Oct 05 10:59:12 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Oct 05 11:10:37 2010 +0200
@@ -234,6 +234,7 @@
 	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
 
 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
+  ATP.thy \
   Big_Operators.thy \
   Code_Evaluation.thy \
   Code_Numeral.thy \

--- a/src/HOL/Sledgehammer.thy	Tue Oct 05 10:59:12 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Tue Oct 05 11:10:37 2010 +0200
@@ -1,18 +1,14 @@
 (*  Title:      HOL/Sledgehammer.thy
     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
-    Author:     Fabian Immler, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 *)
 
 header {* Sledgehammer: Isabelle--ATP Linkup *}
 
 theory Sledgehammer
-imports Plain
-uses "Tools/ATP/atp_problem.ML"
-     "Tools/ATP/atp_proof.ML"
-     "Tools/ATP/atp_systems.ML"
-     "Tools/Sledgehammer/sledgehammer_util.ML"
+imports ATP
+uses "Tools/Sledgehammer/sledgehammer_util.ML"
      "Tools/Sledgehammer/sledgehammer_filter.ML"
      "Tools/Sledgehammer/sledgehammer_translate.ML"
      "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
@@ -22,8 +18,7 @@
 begin
 
 setup {*
-  ATP_Systems.setup
-  #> Sledgehammer.setup
+  Sledgehammer.setup
   #> Sledgehammer_Isar.setup
 *}