remove needless signature entry
authorblanchet
Sat, 03 Jul 2010 00:49:12 +0200
changeset 37703 b4c799bab553
parent 37702 abd5e69bd8cd
child 37704 c6161bee8486
remove needless signature entry
src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Fri Jul 02 17:27:44 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Sat Jul 03 00:49:12 2010 +0200
@@ -12,7 +12,6 @@
   type hol_clause = Metis_Clauses.hol_clause
   type name_pool = string Symtab.table * string Symtab.table
 
-  val type_wrapper_name : string
   val write_tptp_file :
     theory -> bool -> bool -> bool -> Path.T
     -> hol_clause list * hol_clause list * hol_clause list * hol_clause list