--- a/src/HOL/Tools/res_hol_clause.ML Tue Apr 18 05:37:43 2006 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Tue Apr 18 05:38:18 2006 +0200
@@ -478,8 +478,9 @@
(* making axiom and conjecture clauses *)
-fun make_axiom_clause term (ax_name,cls_id) =
- let val term' = comb_of term
+fun make_axiom_clause thm (ax_name,cls_id) =
+ let val term = prop_of thm
+ val term' = comb_of term
val (lits,ctypes_sorts) = literals_of_term term'
val lits' = sort_lits lits
val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
@@ -488,25 +489,18 @@
lits',ctypes_sorts,ctvar_lits,ctfree_lits)
end;
-fun make_axiom_clauses_terms [] = []
- | make_axiom_clauses_terms ((tm,(name,id))::tms) =
- let val cls = make_axiom_clause tm (name,id)
- val clss = make_axiom_clauses_terms tms
- in
- if isTaut cls then clss else (cls::clss)
- end;
-
-fun make_axiom_clauses_thms [] = []
- | make_axiom_clauses_thms ((thm,(name,id))::thms) =
- let val cls = make_axiom_clause (prop_of thm) (name,id)
- val clss = make_axiom_clauses_thms thms
+fun make_axiom_clauses [] = []
+ | make_axiom_clauses ((thm,(name,id))::thms) =
+ let val cls = make_axiom_clause thm (name,id)
+ val clss = make_axiom_clauses thms
in
if isTaut cls then clss else (cls::clss)
end;
-fun make_conjecture_clause n t =
- let val t' = comb_of t
+fun make_conjecture_clause n thm =
+ let val t = prop_of thm
+ val t' = comb_of t
val (lits,ctypes_sorts) = literals_of_term t'
val (ctvar_lits,ctfree_lits) = ResClause.add_typs_aux ctypes_sorts
in
@@ -779,9 +773,9 @@
(* write TPTP format to a single file *)
(* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *)
-fun tptp_write_file terms filename (axclauses,classrel_clauses,arity_clauses) helpers =
- let val clss = make_conjecture_clauses terms
- val axclauses' = make_axiom_clauses_thms axclauses
+fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) helpers =
+ let val clss = make_conjecture_clauses thms
+ val axclauses' = make_axiom_clauses axclauses
val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
val out = TextIO.openOut filename