--- a/src/HOL/Tools/res_atp.ML Mon Jun 22 14:25:22 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Mon Jun 22 17:07:08 2009 +0200
@@ -526,7 +526,7 @@
relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
end;
-(* prepare and count clauses before writing *)
+(* prepare for passing to writer *)
fun prepare_clauses dfg goal_cls chain_ths axcls thy =
let
val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
--- a/src/HOL/Tools/res_hol_clause.ML Mon Jun 22 14:25:22 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Mon Jun 22 17:07:08 2009 +0200
@@ -462,7 +462,6 @@
in (const_min_arity, const_needs_hBOOL) end
else (Symtab.empty, Symtab.empty);
-(* tptp format *)
fun prepare_clauses dfg thy isFO thms ax_tuples user_lemmas =
let
@@ -473,7 +472,8 @@
(clnames, (conjectures, axclauses, helper_clauses))
end
-(* write TPTP format to a single file *)
+(* tptp format *)
+
fun tptp_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
let
val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_counts) conjectures)