# HG changeset patch
# User Philipp Meyer
# Date 1254303239 -7200
# Node ID 1238cbb7c08f92638dbf441b8a69b0dd9ec72eff
# Parent  5e8cef567042fd5e8f3d3998b06ce93f17d7c364
atp_minimal using chain_ths again

diff -r 5e8cef567042 -r 1238cbb7c08f src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Fri Oct 02 23:15:36 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Wed Sep 30 11:33:59 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