remove needless signature entry
authorblanchet
Sat, 03 Jul 2010 00:49:12 +0200
changeset 37694b4c799bab553
parent 37693 abd5e69bd8cd
child 37695 c6161bee8486
remove needless signature entry
src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Fri Jul 02 17:27:44 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Sat Jul 03 00:49:12 2010 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4    type hol_clause = Metis_Clauses.hol_clause
     1.5    type name_pool = string Symtab.table * string Symtab.table
     1.6  
     1.7 -  val type_wrapper_name : string
     1.8    val write_tptp_file :
     1.9      theory -> bool -> bool -> bool -> Path.T
    1.10      -> hol_clause list * hol_clause list * hol_clause list * hol_clause list