--- 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))
--- 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);