# HG changeset patch
# User paulson
# Date 1138012914 -3600
# Node ID aa82bd41555d31285beaac680acb024fd4d6a924
# Parent  c9c6ae9e8b88702d6aff86f12745d372d9427c5a
ResClasimp.get_clasimp_lemmas  now takes all subgoals rather than only the first

diff -r c9c6ae9e8b88 -r aa82bd41555d src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Jan 23 11:38:43 2006 +0100
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Jan 23 11:41:54 2006 +0100
@@ -79,7 +79,7 @@
   val relevant : int ref
   val use_simpset: bool ref
   val get_clasimp_lemmas : 
-         Proof.context -> term -> 
+         Proof.context -> term list -> 
          (ResClause.clause * thm) Array.array * ResClause.clause list 
   end;
 
@@ -317,15 +317,15 @@
 (*Write out the claset and simpset rules of the supplied theory.
   FIXME: argument "goal" is a hack to allow relevance filtering.
   To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
-fun get_clasimp_lemmas ctxt goal = 
+fun get_clasimp_lemmas ctxt goals = 
   let val claset_thms =
-	    map put_name_pair
-	      (ReduceAxiomsN.relevant_filter (!relevant) goal 
+	    map put_name_pair  (*FIXME: relevance filter should use ALL goals*)
+	      (ReduceAxiomsN.relevant_filter (!relevant) (hd goals)
 		(ResAxioms.claset_rules_of_ctxt ctxt))
       val simpset_thms = 
 	    if !use_simpset then 
 		  map put_name_pair 
-		    (ReduceAxiomsN.relevant_filter (!relevant) goal
+		    (ReduceAxiomsN.relevant_filter (!relevant) (hd goals)
 		      (ResAxioms.simpset_rules_of_ctxt ctxt))
 	    else []
       val banned = make_banned_test (map #1 (claset_thms@simpset_thms))
diff -r c9c6ae9e8b88 -r aa82bd41555d src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Jan 23 11:38:43 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML	Mon Jan 23 11:41:54 2006 +0100
@@ -136,9 +136,8 @@
 (*We write out problem files for each subgoal. Argument pf generates filenames,
   and allows the suppression of the suffix "_1" in problem-generation mode.*)
 fun write_problem_files pf (ctxt,th)  =
-  let val prems = Thm.prems_of th
-      val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
-              (*FIXME: hack!! need to consider relevance for all prems*)
+  let val goals = Thm.prems_of th
+      val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt goals 
       val _ = Output.debug ("claset and simprules total clauses = " ^ 
                      Int.toString (Array.length clause_arr))
       val thy = ProofContext.theory_of ctxt
@@ -157,7 +156,7 @@
 		       (axclauses,classrel_clauses,arity_clauses);
 		 all_tac))]) n th;
 	    pf n :: writenext (n-1))
-      in (writenext (length prems), clause_arr) end;
+      in (writenext (length goals), clause_arr) end;
 
 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
                                     Posix.Process.pid * string list) option);