# HG changeset patch
# User blanchet
# Date 1280246161 -7200
# Node ID e024504943d1d60751ee6862e3cc61559cb04f6d
# Parent  badd89633f4ced1a718310521c8a31326e40d6fd
rename "ATP_Manager" ML module to "Sledgehammer";
more refactoring to come

diff -r badd89633f4c -r e024504943d1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 27 17:49:16 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 27 17:56:01 2010 +0200
@@ -269,7 +269,6 @@
   $(SRC)/Provers/Arith/extract_common_term.ML \
   $(SRC)/Tools/Metis/metis.ML \
   Tools/ATP_Manager/async_manager.ML \
-  Tools/ATP_Manager/atp_manager.ML \
   Tools/ATP_Manager/atp_problem.ML \
   Tools/ATP_Manager/atp_systems.ML \
   Tools/choice_specification.ML \
@@ -320,6 +319,7 @@
   Tools/Sledgehammer/meson_tactic.ML \
   Tools/Sledgehammer/metis_clauses.ML \
   Tools/Sledgehammer/metis_tactics.ML \
+  Tools/Sledgehammer/sledgehammer.ML \
   Tools/Sledgehammer/sledgehammer_fact_filter.ML \
   Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \
   Tools/Sledgehammer/sledgehammer_isar.ML \
diff -r badd89633f4c -r e024504943d1 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Jul 27 17:49:16 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 17:56:01 2010 +0200
@@ -97,7 +97,7 @@
 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_manager.ML"
+use "Tools/Sledgehammer/sledgehammer.ML"
 use "Tools/ATP_Manager/atp_systems.ML"
 setup ATP_Systems.setup
 use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
diff -r badd89633f4c -r e024504943d1 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:49:16 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 17:56:01 2010 +0200
@@ -24,7 +24,7 @@
 open Sledgehammer_Fact_Filter
 open ATP_Problem
 open Sledgehammer_Proof_Reconstruct
-open ATP_Manager
+open Sledgehammer
 
 val trace = Unsynchronized.ref false
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
diff -r badd89633f4c -r e024504943d1 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 27 17:49:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 27 17:56:01 2010 +0200
@@ -1,12 +1,12 @@
-(*  Title:      HOL/Tools/ATP_Manager/atp_manager.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer.ML
     Author:     Fabian Immler, TU Muenchen
     Author:     Makarius
     Author:     Jasmin Blanchette, TU Muenchen
 
-Central manager component for ATP threads.
+Sledgehammer's heart.
 *)
 
-signature ATP_MANAGER =
+signature SLEDGEHAMMER =
 sig
   type relevance_override = Sledgehammer_Fact_Filter.relevance_override
   type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
@@ -59,7 +59,7 @@
     -> Proof.state -> string -> unit
 end;
 
-structure ATP_Manager : ATP_MANAGER =
+structure Sledgehammer : SLEDGEHAMMER =
 struct
 
 open Metis_Clauses
diff -r badd89633f4c -r e024504943d1 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jul 27 17:49:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jul 27 17:56:01 2010 +0200
@@ -7,8 +7,8 @@
 
 signature SLEDGEHAMMER_FACT_MINIMIZER =
 sig
-  type params = ATP_Manager.params
-  type prover_result = ATP_Manager.prover_result
+  type params = Sledgehammer.params
+  type prover_result = Sledgehammer.prover_result
 
   val minimize_theorems :
     params -> int -> int -> Proof.state -> (string * thm list) list
@@ -21,7 +21,7 @@
 open Metis_Clauses
 open Sledgehammer_Util
 open Sledgehammer_Proof_Reconstruct
-open ATP_Manager
+open Sledgehammer
 
 (* wrapper for calling external prover *)
 
diff -r badd89633f4c -r e024504943d1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jul 27 17:49:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jul 27 17:56:01 2010 +0200
@@ -6,7 +6,7 @@
 
 signature SLEDGEHAMMER_ISAR =
 sig
-  type params = ATP_Manager.params
+  type params = Sledgehammer.params
 
   val atps: string Unsynchronized.ref
   val timeout: int Unsynchronized.ref
@@ -19,7 +19,7 @@
 
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
-open ATP_Manager
+open Sledgehammer
 open ATP_Systems
 open Sledgehammer_Fact_Minimizer