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