src/HOL/Tools/res_atp.ML
changeset 21563 b4718f2c15f0
parent 21509 6c5755ad9cae
child 21588 cd0dc678a205
     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