src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 40068 ed2869dd9bfa
parent 40067 0783415ed7f0
child 40069 6f7bf79b1506
--- 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