# HG changeset patch
# User blanchet
# Date 1280249155 -7200
# Node ID b660597a6796a6e46ef1b959ee4306737c581f54
# Parent  e4a95eb5530e7925af8957af8e2cba7ae6dd4d39
reorder ML files in theory

diff -r e4a95eb5530e -r b660597a6796 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Jul 27 18:38:10 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 18:45:55 2010 +0200
@@ -10,17 +10,17 @@
 theory Sledgehammer
 imports Plain Hilbert_Choice
 uses
-  "~~/src/Tools/Metis/metis.ML"
+  ("Tools/ATP_Manager/async_manager.ML")
+  ("Tools/ATP_Manager/atp_problem.ML")
+  ("Tools/ATP_Manager/atp_systems.ML")
+  ("~~/src/Tools/Metis/metis.ML")
   ("Tools/Sledgehammer/clausifier.ML")
   ("Tools/Sledgehammer/meson_tactic.ML")
   ("Tools/Sledgehammer/metis_clauses.ML")
   ("Tools/Sledgehammer/metis_tactics.ML")
   ("Tools/Sledgehammer/sledgehammer_util.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
-  ("Tools/ATP_Manager/atp_problem.ML")
   ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
-  ("Tools/ATP_Manager/async_manager.ML")
-  ("Tools/ATP_Manager/atp_systems.ML")
   ("Tools/Sledgehammer/sledgehammer.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML")
   ("Tools/Sledgehammer/sledgehammer_isar.ML")
@@ -85,6 +85,12 @@
 apply (simp add: COMBC_def) 
 done
 
+use "Tools/ATP_Manager/async_manager.ML"
+use "Tools/ATP_Manager/atp_problem.ML"
+use "Tools/ATP_Manager/atp_systems.ML"
+setup ATP_Systems.setup
+
+use "~~/src/Tools/Metis/metis.ML"
 use "Tools/Sledgehammer/clausifier.ML"
 use "Tools/Sledgehammer/meson_tactic.ML"
 setup Meson_Tactic.setup
@@ -94,11 +100,7 @@
 
 use "Tools/Sledgehammer/sledgehammer_util.ML"
 use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
-use "Tools/ATP_Manager/atp_problem.ML"
 use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
-use "Tools/ATP_Manager/async_manager.ML"
-use "Tools/ATP_Manager/atp_systems.ML"
-setup ATP_Systems.setup
 use "Tools/Sledgehammer/sledgehammer.ML"
 setup Sledgehammer.setup
 use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
diff -r e4a95eb5530e -r b660597a6796 src/HOL/Tools/ATP_Manager/atp_problem.ML
--- a/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 18:38:10 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 18:45:55 2010 +0200
@@ -32,8 +32,6 @@
 structure ATP_Problem : ATP_PROBLEM =
 struct
 
-open Sledgehammer_Util
-
 (** ATP problem **)
 
 datatype 'a fo_term = ATerm of 'a * 'a fo_term list