# 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