Goals in clause form are sent to the relevance filter.
authormengj
Mon Nov 27 23:47:42 2006 +0100 (2006-11-27)
changeset 21563b4718f2c15f0
parent 21562 dd39c9e62f19
child 21564 519ee3129ee1
Goals in clause form are sent to the relevance filter.
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Nov 27 21:07:00 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Nov 27 23:47:42 2006 +0100
     1.3 @@ -863,8 +863,7 @@
     1.4        val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
     1.5        val white_cls = ResAxioms.cnf_rules_pairs white_thms
     1.6        (*clauses relevant to goal gl*)
     1.7 -      val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
     1.8 -                           goals
     1.9 +      val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
    1.10        val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
    1.11                    axcls_list
    1.12        val keep_types = if is_fol_logic logic then !ResClause.keep_types