# HG changeset patch
# User nipkow
# Date 1254632482 -7200
# Node ID 6eafaa92a95ed9f238540e63b999f2671ccb3718
# Parent  f8d1e16ec7580d7684035579c66b46b8eaaf3bb7# Parent  1238cbb7c08f92638dbf441b8a69b0dd9ec72eff
merged

diff -r f8d1e16ec758 -r 6eafaa92a95e src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Sat Oct 03 12:10:16 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Sun Oct 04 07:01:22 2009 +0200
@@ -517,6 +517,9 @@
     | Fol => true
     | Hol => false
 
+fun ths_to_cls thy ths =
+  ResAxioms.cnf_rules_pairs thy (filter check_named (map ResAxioms.pairname ths))
+
 fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
   let
     val thy = ProofContext.theory_of ctxt
@@ -526,9 +529,8 @@
                                      |> restrict_to_logic thy isFO
                                      |> remove_unwanted_clauses
     val axcls = relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
-    val white_thms = filter check_named (map ResAxioms.pairname
-      (whitelist_fo @ (if isFO then [] else whitelist_ho) @ chain_ths))
-    val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
+    (* add whitelist *)
+    val white_cls = ths_to_cls thy (whitelist_fo @ (if isFO then [] else whitelist_ho))
   in
     white_cls @ axcls 
   end;
@@ -537,6 +539,10 @@
    create additional clauses based on the information from extra_cls *)
 fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   let
+    (* add chain thms *)
+    val chain_cls = ths_to_cls thy chain_ths
+    val axcls = chain_cls @ axcls
+    val extra_cls = chain_cls @ extra_cls
     val isFO = isFO thy goal_cls
     val ccls = subtract_cls goal_cls extra_cls
     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls