src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML

-(*  Title:      HOL/Tools/res_clause.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
     Author:     Jia Meng, Cambridge University Computer Laboratory
 
 Storing/printing FOL clauses and arity clauses.  Typed equality is
 treated differently.
 
 FIXME: combine with res_hol_clause!
 *)
 
-signature RES_CLAUSE =
+signature SLEDGEHAMMER_FOL_CLAUSE =
 sig
   val schematic_var_prefix: string
   val fixed_var_prefix: string
   val tvar_prefix: string
   val tfree_prefix: string

   val tptp_tfree_clause : string -> string
   val tptp_arity_clause : arityClause -> string
   val tptp_classrelClause : classrelClause -> string
 end
 
-structure Res_Clause: RES_CLAUSE =
+structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
 struct
 
 val schematic_var_prefix = "V_";
 val fixed_var_prefix = "v_";