src/HOL/Tools/ATP/res_clasimpset.ML
changeset 18753 aa82bd41555d
parent 18677 01265301db7f
child 18792 fb427f4a01f2
     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))