# 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