# HG changeset patch
# User mengj
# Date 1145331498 -7200
# Node ID 085568445283a7ad3dbc6b5cf8c80566d661e278
# Parent  e32a4703d8341b8fa66f48559ada249196ffdbb1
Take conjectures and axioms as thms when convert them to ResHolClause.clause format.

diff -r e32a4703d834 -r 085568445283 src/HOL/Tools/res_hol_clause.ML
--- 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