1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Jan 23 11:38:43 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Mon Jan 23 11:41:54 2006 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4    val relevant : int ref
     1.5    val use_simpset: bool ref
     1.6    val get_clasimp_lemmas : 
     1.7 -         Proof.context -> term -> 
     1.8 +         Proof.context -> term list -> 
     1.9           (ResClause.clause * thm) Array.array * ResClause.clause list 
    1.10    end;
    1.11  
    1.12 @@ -317,15 +317,15 @@
    1.13  (*Write out the claset and simpset rules of the supplied theory.
    1.14    FIXME: argument "goal" is a hack to allow relevance filtering.
    1.15    To reduce the number of clauses produced, set ResClasimp.relevant:=1*)
    1.16 -fun get_clasimp_lemmas ctxt goal = 
    1.17 +fun get_clasimp_lemmas ctxt goals = 
    1.18    let val claset_thms =
    1.19 -	    map put_name_pair
    1.20 -	      (ReduceAxiomsN.relevant_filter (!relevant) goal 
    1.21 +	    map put_name_pair  (*FIXME: relevance filter should use ALL goals*)
    1.22 +	      (ReduceAxiomsN.relevant_filter (!relevant) (hd goals)
    1.23  		(ResAxioms.claset_rules_of_ctxt ctxt))
    1.24        val simpset_thms = 
    1.25  	    if !use_simpset then 
    1.26  		  map put_name_pair 
    1.27 -		    (ReduceAxiomsN.relevant_filter (!relevant) goal
    1.28 +		    (ReduceAxiomsN.relevant_filter (!relevant) (hd goals)
    1.29  		      (ResAxioms.simpset_rules_of_ctxt ctxt))
    1.30  	    else []
    1.31        val banned = make_banned_test (map #1 (claset_thms@simpset_thms))

     2.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jan 23 11:38:43 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Jan 23 11:41:54 2006 +0100
     2.3 @@ -136,9 +136,8 @@
     2.4  (*We write out problem files for each subgoal. Argument pf generates filenames,
     2.5    and allows the suppression of the suffix "_1" in problem-generation mode.*)
     2.6  fun write_problem_files pf (ctxt,th)  =
     2.7 -  let val prems = Thm.prems_of th
     2.8 -      val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
     2.9 -              (*FIXME: hack!! need to consider relevance for all prems*)
    2.10 +  let val goals = Thm.prems_of th
    2.11 +      val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt goals 
    2.12        val _ = Output.debug ("claset and simprules total clauses = " ^ 
    2.13                       Int.toString (Array.length clause_arr))
    2.14        val thy = ProofContext.theory_of ctxt
    2.15 @@ -157,7 +156,7 @@
    2.16  		       (axclauses,classrel_clauses,arity_clauses);
    2.17  		 all_tac))]) n th;
    2.18  	    pf n :: writenext (n-1))
    2.19 -      in (writenext (length prems), clause_arr) end;
    2.20 +      in (writenext (length goals), clause_arr) end;
    2.21  
    2.22  val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
    2.23                                      Posix.Process.pid * string list) option);