Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
always include whitelist;
authorimmler@in.tum.de
Sun, 28 Jun 2009 15:01:28 +0200
changeset 31836 8a8cf7b44739
parent 31835 b686d4df54c2
child 31837 a50de97f1b08
always include whitelist;
src/HOL/Tools/res_atp.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle