src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
changeset 38988 483879af0643
parent 38986 e34c1b09bb5e
child 39106 5ab6a3707499
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Aug 31 23:50:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Aug 31 23:50:59 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Claire Quigley, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
@@ -6,9 +6,9 @@
 Transfer of proofs from external provers.
 *)
 
-signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
+signature SLEDGEHAMMER_RECONSTRUCT =
 sig
-  type locality = Sledgehammer_Fact_Filter.locality
+  type locality = Sledgehammer_Filter.locality
   type minimize_command = string list -> string
   type metis_params =
     bool * minimize_command * string * (string * locality) list vector * thm
@@ -22,13 +22,13 @@
   val proof_text : bool -> isar_params -> metis_params -> text_result
 end;
 
-structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
+structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
 struct
 
 open ATP_Problem
 open Metis_Clauses
 open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
+open Sledgehammer_Filter
 open Sledgehammer_Translate
 
 type minimize_command = string list -> string