# HG changeset patch
# User mengj
# Date 1144379571 -7200
# Node ID aebf9dddccd7e501d79201c5d3c482c96f266550
# Parent  36b6b15ee6707dd636d8f06a8b5a18b02eb81fb4
tptp_write_file accepts axioms as thm.

diff -r 36b6b15ee670 -r aebf9dddccd7 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Fri Apr 07 05:12:23 2006 +0200
+++ b/src/HOL/Tools/res_clause.ML	Fri Apr 07 05:12:51 2006 +0200
@@ -55,7 +55,7 @@
   val tptp_classrelClause : classrelClause -> string
   val tptp_of_typeLit : type_literal -> string
   val tptp_tfree_clause : string -> string
-  val tptp_write_file: term list -> string -> ((Term.term * (string * int)) list * classrelClause list * arityClause list) -> unit
+  val tptp_write_file: term list -> string -> ((thm * (string * int)) list * classrelClause list * arityClause list) -> unit
   val tvar_prefix : string
   val types_eq: fol_type list * fol_type list -> (string*string) list * (string*string) list -> bool * ((string*string) list * (string*string) list)
   val types_ord : fol_type list * fol_type list -> order
@@ -620,6 +620,11 @@
     case make_axiom_clause tm (name,id) of SOME cls => if isTaut cls then make_axiom_clauses_terms tms else cls :: make_axiom_clauses_terms tms
 						    | NONE => make_axiom_clauses_terms tms;
     
+fun make_axiom_clauses_thms [] = []
+  | make_axiom_clauses_thms ((thm,(name,id))::thms) =
+    case make_axiom_clause (prop_of thm) (name,id) of SOME cls => if isTaut cls then make_axiom_clauses_thms thms else cls :: make_axiom_clauses_thms thms
+						    | NONE => make_axiom_clauses_thms thms;
+
 (**** Isabelle arities ****)
 
 exception ARCLAUSE of string;
@@ -1030,7 +1035,7 @@
   let
     val _ = Output.debug ("Preparing to write the TPTP file " ^ filename)
     val clss = make_conjecture_clauses terms
-    val axclauses' = make_axiom_clauses_terms axclauses
+    val axclauses' = make_axiom_clauses_thms axclauses
     val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
     val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
     val out = TextIO.openOut filename
@@ -1043,4 +1048,8 @@
     TextIO.closeOut out
   end;
 
+
+
+
+
 end;
diff -r 36b6b15ee670 -r aebf9dddccd7 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Fri Apr 07 05:12:23 2006 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Fri Apr 07 05:12:51 2006 +0200
@@ -496,6 +496,15 @@
 	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
+    in
+	if isTaut cls then clss else (cls::clss)
+    end;
+
+
 fun make_conjecture_clause n t =
     let val t' = comb_of t
 	val (lits,ctypes_sorts) = literals_of_term t'
@@ -772,7 +781,7 @@
 (* 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_terms axclauses
+	val axclauses' = make_axiom_clauses_thms 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