src/HOL/Tools/res_atp.ML
changeset 32866 1238cbb7c08f
parent 32552 4d4ee06e9420
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Oct 02 23:15:36 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Sep 30 11:33:59 2009 +0200
     1.3 @@ -517,6 +517,9 @@
     1.4      | Fol => true
     1.5      | Hol => false
     1.6  
     1.7 +fun ths_to_cls thy ths =
     1.8 +  ResAxioms.cnf_rules_pairs thy (filter check_named (map ResAxioms.pairname ths))
     1.9 +
    1.10  fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
    1.11    let
    1.12      val thy = ProofContext.theory_of ctxt
    1.13 @@ -526,9 +529,8 @@
    1.14                                       |> restrict_to_logic thy isFO
    1.15                                       |> remove_unwanted_clauses
    1.16      val axcls = relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
    1.17 -    val white_thms = filter check_named (map ResAxioms.pairname
    1.18 -      (whitelist_fo @ (if isFO then [] else whitelist_ho) @ chain_ths))
    1.19 -    val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
    1.20 +    (* add whitelist *)
    1.21 +    val white_cls = ths_to_cls thy (whitelist_fo @ (if isFO then [] else whitelist_ho))
    1.22    in
    1.23      white_cls @ axcls 
    1.24    end;
    1.25 @@ -537,6 +539,10 @@
    1.26     create additional clauses based on the information from extra_cls *)
    1.27  fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
    1.28    let
    1.29 +    (* add chain thms *)
    1.30 +    val chain_cls = ths_to_cls thy chain_ths
    1.31 +    val axcls = chain_cls @ axcls
    1.32 +    val extra_cls = chain_cls @ extra_cls
    1.33      val isFO = isFO thy goal_cls
    1.34      val ccls = subtract_cls goal_cls extra_cls
    1.35      val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls