# HG changeset patch
# User mengj
# Date 1164667662 -3600
# Node ID b4718f2c15f0ae28ae611f6303a0622f46aac2ac
# Parent  dd39c9e62f19eb8f44064541ed451bb6651a8aea
Goals in clause form are sent to the relevance filter.

diff -r dd39c9e62f19 -r b4718f2c15f0 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Nov 27 21:07:00 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML	Mon Nov 27 23:47:42 2006 +0100
@@ -863,8 +863,7 @@
       val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
       val white_cls = ResAxioms.cnf_rules_pairs white_thms
       (*clauses relevant to goal gl*)
-      val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
-                           goals
+      val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
       val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
                   axcls_list
       val keep_types = if is_fol_logic logic then !ResClause.keep_types