# HG changeset patch
# User immler@in.tum.de
# Date 1246194088 -7200
# Node ID 8a8cf7b4473928cc5a2916f6b0dd4b49cf8de7ce
# Parent  b686d4df54c285aa7e7093dc89f54a52d0a39870
always include whitelist;

diff -r b686d4df54c2 -r 8a8cf7b44739 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Sun Jun 28 15:01:28 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Sun Jun 28 15:01:28 2009 +0200
@@ -532,9 +532,10 @@
 fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   let
     val white_thms =
-      filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
+      filter check_named (map ResAxioms.pairname (whitelist @ chain_ths))
     val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
     val extra_cls = white_cls @ extra_cls
+    val axcls = white_cls @ axcls
     val ccls = subtract_cls goal_cls extra_cls
     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
     val ccltms = map prop_of ccls