# HG changeset patch
# User mengj
# Date 1152964330 -7200
# Node ID c89ee2f4efd560b534f2b66764e1b2e7f9672501
# Parent  5303e59282855dda7018e4585c60ead4e85f62cc
Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.

diff -r 5303e5928285 -r c89ee2f4efd5 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Sat Jul 15 13:50:26 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Sat Jul 15 13:52:10 2006 +0200
@@ -586,15 +586,15 @@
 
 val linkup_logic_mode = ref Auto;
 
-fun tptp_writer logic goals filename (axioms,classrels,arities) =
+fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
     if is_fol_logic logic 
     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
-    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities);
+    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
 
-fun dfg_writer logic goals filename (axioms,classrels,arities) =
+fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
     if is_fol_logic logic 
     then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
-    else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities);
+    else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
 
 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
@@ -602,6 +602,7 @@
 	val hyp_cls = cnf_hyps_thms ctxt
 	val goal_cls = conj_cls@hyp_cls
 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
+	val user_lemmas_names = map #1 user_rules
 	val rm_black_cls = blacklist_filter included_thms 
 	val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls
 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
@@ -618,7 +619,7 @@
         val writer = if dfg then dfg_writer else tptp_writer 
 	val file = atp_input_file()
     in
-	(writer prob_logic goal_cls file (axclauses,classrel_clauses,arity_clauses);
+	(writer prob_logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
 	 Output.debug ("Writing to " ^ file);
 	 file)
     end;
@@ -734,7 +735,7 @@
       val writer = if !prover = "spass" then dfg_writer else tptp_writer 
       fun write_all [] _ = []
 	| write_all (sub::subgoals) k =
-	   (writer goals_logic sub (probfile k) (axclauses,classrel_clauses,arity_clauses),
+	   (writer goals_logic sub (probfile k) (axclauses,classrel_clauses,arity_clauses) [],
 	    probfile k) :: write_all subgoals (k-1)
       val (clnames::_, filenames) = ListPair.unzip (write_all neg_subgoals (length goals))
       val thm_names = Array.fromList clnames