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