src/HOL/Tools/Sledgehammer/sledgehammer.ML

 *)
 
 signature SLEDGEHAMMER =
 sig
   type failure = ATP_Systems.failure
-  type locality = Sledgehammer_Fact_Filter.locality
-  type relevance_override = Sledgehammer_Fact_Filter.relevance_override
-  type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
+  type locality = Sledgehammer_Filter.locality
+  type relevance_override = Sledgehammer_Filter.relevance_override
+  type minimize_command = Sledgehammer_Reconstruct.minimize_command
   type params =
     {blocking: bool,
      debug: bool,
      verbose: bool,
      overlord: bool,

 
 open ATP_Problem
 open ATP_Systems
 open Metis_Clauses
 open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
+open Sledgehammer_Filter
 open Sledgehammer_Translate
-open Sledgehammer_Proof_Reconstruct
+open Sledgehammer_Reconstruct
 
 
 (** The Sledgehammer **)
 
 (* Identifier to distinguish Sledgehammer from other tools using

 val extract_clause_formula_relation =
   Substring.full #> Substring.position set_ClauseFormulaRelationN
   #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
   #> explode #> parse_clause_formula_relation #> fst
 
-(* TODO: move to "Sledgehammer_Proof_Reconstruct.ML" *)
+(* TODO: move to "Sledgehammer_Reconstruct" *)
 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
                                               axiom_names =
   if String.isSubstring set_ClauseFormulaRelationN output then
     (* This is a hack required for keeping track of axioms after they have been
        clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is