--- 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 **)
--- 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
--- 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
--- 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 *)