# HG changeset patch
# User wenzelm
# Date 1213302589 -7200
# Node ID 9e4475b9d58c608cdb3c51eb240caedf7586ff20
# Parent  e1e9b210d69975b5b25545395df2705fb4452431
tuned setup;

diff -r e1e9b210d699 -r 9e4475b9d58c src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Thu Jun 12 22:14:07 2008 +0200
+++ b/src/HOL/ATP_Linkup.thy	Thu Jun 12 22:29:49 2008 +0200
@@ -8,7 +8,6 @@
 
 theory ATP_Linkup
 imports Record Presburger SAT Recdef Extraction Relation_Power Hilbert_Choice
-   (*FIXME It must be a parent or a child of every other theory, to prevent theory-merge errors. FIXME*)
 uses
   "Tools/polyhash.ML"
   "Tools/res_clause.ML"
@@ -89,15 +88,14 @@
 apply (simp add: COMBC_def) 
 done
 
+use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
+setup ResAxioms.setup
 
-use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
 use "Tools/res_hol_clause.ML"
 use "Tools/res_reconstruct.ML"
 use "Tools/watcher.ML"
 use "Tools/res_atp.ML"
 
-setup ResAxioms.meson_method_setup
-
 
 subsection {* Setup for Vampire, E prover and SPASS *}
 
@@ -110,15 +108,11 @@
 use "Tools/res_atp_methods.ML"
 setup ResAtpMethods.setup      --{*Oracle ATP methods: still useful?*}
 setup ResReconstruct.setup     --{*Config parameters*}
-setup ResAxioms.setup          --{*Sledgehammer*}
+
 
 subsection {* The Metis prover *}
 
 use "Tools/metis_tools.ML"
 setup MetisTools.setup
 
-setup {*
-  Theory.at_end ResAxioms.clause_cache_endtheory
-*}
-
 end