# HG changeset patch
# User blanchet
# Date 1288088239 -7200
# Node ID 00152d17855bc2efdae007aebbdb620b0764b77c
# Parent  d3bc972b7d9d19fee48fca20a3967df0459eed7e
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers

diff -r d3bc972b7d9d -r 00152d17855b src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/ATP.thy	Tue Oct 26 12:17:19 2010 +0200
@@ -6,11 +6,10 @@
 header {* Automatic Theorem Provers (ATPs) *}
 
 theory ATP
-imports HOL
-uses
-  "Tools/ATP/atp_problem.ML"
-  "Tools/ATP/atp_proof.ML"
-  "Tools/ATP/atp_systems.ML"
+imports Plain
+uses "Tools/ATP/atp_problem.ML"
+     "Tools/ATP/atp_proof.ML"
+     "Tools/ATP/atp_systems.ML"
 begin
 
 setup ATP_Systems.setup
diff -r d3bc972b7d9d -r 00152d17855b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Oct 26 12:17:19 2010 +0200
@@ -144,7 +144,6 @@
 	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
 
 PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
-  ATP.thy \
   Complete_Lattice.thy \
   Complete_Partial_Order.thy \
   Datatype.thy \
@@ -170,7 +169,6 @@
   Rings.thy \
   SAT.thy \
   Set.thy \
-  Sledgehammer.thy \
   Sum_Type.thy \
   Tools/abel_cancel.ML \
   Tools/arith_data.ML \
@@ -239,6 +237,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 \
@@ -269,6 +268,7 @@
   Refute.thy \
   Semiring_Normalization.thy \
   SetInterval.thy \
+  Sledgehammer.thy \
   SMT.thy \
   String.thy \
   Typerep.thy \
diff -r d3bc972b7d9d -r 00152d17855b src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/Main.thy	Tue Oct 26 12:17:19 2010 +0200
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Record Predicate_Compile Nitpick SMT Quotient
+imports Plain Record Predicate_Compile Nitpick SMT
 begin
 
 text {*
diff -r d3bc972b7d9d -r 00152d17855b src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/Plain.thy	Tue Oct 26 12:17:19 2010 +0200
@@ -1,7 +1,7 @@
 header {* Plain HOL *}
 
 theory Plain
-imports Datatype FunDef Extraction Sledgehammer
+imports Datatype FunDef Extraction Metis
 begin
 
 text {*
diff -r d3bc972b7d9d -r 00152d17855b src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/Refute.thy	Tue Oct 26 12:17:19 2010 +0200
@@ -8,7 +8,7 @@
 header {* Refute *}
 
 theory Refute
-imports Hilbert_Choice List
+imports Hilbert_Choice List Sledgehammer
 uses "Tools/refute.ML"
 begin
 
diff -r d3bc972b7d9d -r 00152d17855b src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Tue Oct 26 12:17:19 2010 +0200
@@ -7,7 +7,7 @@
 header {* Sledgehammer: Isabelle--ATP Linkup *}
 
 theory Sledgehammer
-imports ATP Metis
+imports ATP
 uses "Tools/Sledgehammer/sledgehammer_util.ML"
      "Tools/Sledgehammer/sledgehammer_filter.ML"
      "Tools/Sledgehammer/sledgehammer_atp_translate.ML"