# HG changeset patch
# User blanchet
# Date 1287748674 -7200
# Node ID ed2869dd9bfadcad8ae7f2054590c56c2a59b429
# Parent  0783415ed7f067520531367c2e927e593890e672
renamed modules

diff -r 0783415ed7f0 -r ed2869dd9bfa src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 13:54:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 13:57:54 2010 +0200
@@ -11,8 +11,8 @@
   type failure = ATP_Systems.failure
   type locality = Sledgehammer_Filter.locality
   type relevance_override = Sledgehammer_Filter.relevance_override
-  type fol_formula = Sledgehammer_Translate.fol_formula
-  type minimize_command = Sledgehammer_Reconstruct.minimize_command
+  type fol_formula = Sledgehammer_ATP_Translate.fol_formula
+  type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
 
   type params =
     {blocking: bool,
@@ -74,8 +74,8 @@
 open Metis_Translate
 open Sledgehammer_Util
 open Sledgehammer_Filter
-open Sledgehammer_Translate
-open Sledgehammer_Reconstruct
+open Sledgehammer_ATP_Translate
+open Sledgehammer_ATP_Reconstruct
 
 
 (** The Sledgehammer **)
diff -r 0783415ed7f0 -r ed2869dd9bfa src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 13:54:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Oct 22 13:57:54 2010 +0200
@@ -6,7 +6,7 @@
 Proof reconstruction for Sledgehammer.
 *)
 
-signature SLEDGEHAMMER_RECONSTRUCT =
+signature SLEDGEHAMMER_ATP_RECONSTRUCT =
 sig
   type locality = Sledgehammer_Filter.locality
   type minimize_command = string list -> string
@@ -29,7 +29,7 @@
   val proof_text : bool -> isar_params -> metis_params -> text_result
 end;
 
-structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
+structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT =
 struct
 
 open ATP_Problem
diff -r 0783415ed7f0 -r ed2869dd9bfa src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Oct 22 13:54:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Oct 22 13:57:54 2010 +0200
@@ -6,7 +6,7 @@
 Translation of HOL to FOL for Sledgehammer.
 *)
 
-signature SLEDGEHAMMER_TRANSLATE =
+signature SLEDGEHAMMER_ATP_TRANSLATE =
 sig
   type 'a problem = 'a ATP_Problem.problem
   type fol_formula
@@ -22,7 +22,7 @@
     -> string problem * string Symtab.table * int * (string * 'a) list vector
 end;
 
-structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
+structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
 struct
 
 open ATP_Problem
diff -r 0783415ed7f0 -r ed2869dd9bfa src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 13:54:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 13:57:54 2010 +0200
@@ -23,7 +23,6 @@
 open ATP_Proof
 open Sledgehammer_Util
 open Sledgehammer_Filter
-open Sledgehammer_Translate
 open Sledgehammer
 
 (* wrapper for calling external prover *)