author | blanchet |
Sat, 03 Jul 2010 00:49:12 +0200 | |
changeset 37703 | b4c799bab553 |
parent 37702 | abd5e69bd8cd |
child 37704 | c6161bee8486 |
src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML | file | annotate | diff | comparison | revisions |
--- 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