# HG changeset patch
# User blanchet
# Date 1277472638 -7200
# Node ID 76e23303c7ffa4b7058caa3ca33bac2ce0191e25
# Parent  de5feddaa95cb756a0144504ab40403b5ad3ac2d
more moving around of ML files in "Sledgehammer.thy"

diff -r de5feddaa95c -r 76e23303c7ff src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Fri Jun 25 15:22:12 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Fri Jun 25 15:30:38 2010 +0200
@@ -11,16 +11,16 @@
 imports Plain Hilbert_Choice
 uses
   "~~/src/Tools/Metis/metis.ML"
-  "Tools/Sledgehammer/sledgehammer_util.ML"
-  ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
   ("Tools/Sledgehammer/meson_tactic.ML")
+  ("Tools/Sledgehammer/sledgehammer_util.ML")
+  ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
   ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
-  ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
   ("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
   ("Tools/ATP_Manager/atp_manager.ML")
   ("Tools/ATP_Manager/atp_systems.ML")
+  ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
   ("Tools/Sledgehammer/sledgehammer_isar.ML")
   ("Tools/Sledgehammer/metis_tactics.ML")
@@ -85,19 +85,20 @@
 apply (simp add: COMBC_def) 
 done
 
-
-use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
 setup Sledgehammer_Fact_Preprocessor.setup
 use "Tools/Sledgehammer/meson_tactic.ML"
 setup Meson_Tactic.setup
+
+use "Tools/Sledgehammer/sledgehammer_util.ML"
+use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
 use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
-use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
 use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
 use "Tools/ATP_Manager/atp_manager.ML"
 use "Tools/ATP_Manager/atp_systems.ML"
 setup ATP_Systems.setup
+use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
 use "Tools/Sledgehammer/sledgehammer_isar.ML"
 use "Tools/Sledgehammer/metis_tactics.ML"
diff -r de5feddaa95c -r 76e23303c7ff src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 15:22:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 25 15:30:38 2010 +0200
@@ -35,8 +35,6 @@
 structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
 struct
 
-open Sledgehammer_FOL_Clause
-
 type cnf_thm = thm * ((string * int) * thm)
 
 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator