# HG changeset patch
# User mengj
# Date 1144379520 -7200
# Node ID 1a07f6cf1e6c71ec932011ae981d33127accbaf8
# Parent  c33563c7c14cc0c4873e4e4c16a52bccc806a962
lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.

diff -r c33563c7c14c -r 1a07f6cf1e6c src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Fri Apr 07 03:20:34 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Fri Apr 07 05:12:00 2006 +0200
@@ -364,7 +364,7 @@
 	val hyp_cls = map prop_of (cnf_hyps_thms ctxt)
 	val goal_cls = conj_cls@hyp_cls
 	val user_rules = map ResAxioms.pairname user_thms
-	val (names_arr,axclauses_as_tms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
+	val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
 	val thy = ProofContext.theory_of ctxt
 	val prob_logic = case mode of Auto => problem_logic_goals [goal_cls]
 				    | Fol => FOL
@@ -375,7 +375,7 @@
 	val writer = tptp_writer
 	val file = atp_input_file()
     in
-	(writer prob_logic goal_cls file (axclauses_as_tms,classrel_clauses,arity_clauses);
+	(writer prob_logic goal_cls file (axclauses_as_thms,classrel_clauses,arity_clauses);
 	 warning ("Writing to " ^ file);
 	 file)
     end;