--- 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