# HG changeset patch
# User blanchet
# Date 1278110952 -7200
# Node ID b4c799bab553bf9c7f2cf4ed8c0b1b1208f3537f
# Parent  abd5e69bd8cdbd14c33cb76ebc23d532ab4c28da
remove needless signature entry

diff -r abd5e69bd8cd -r b4c799bab553 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