src/HOL/Tools/res_atp.ML

                                        |> restrict_to_logic logic
                                        |> remove_unwanted_clauses
       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 
                        else is_typed_hol ()
       val writer = if !prover = "spass" then dfg_writer else tptp_writer