--- a/src/HOL/Tools/res_atp.ML Wed Jun 03 16:56:41 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Wed Jun 03 16:56:41 2009 +0200
@@ -8,7 +8,7 @@
val type_consts_of_terms : theory -> term list -> string list
val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
(thm * (string * int)) list
- val prepare_clauses : bool -> thm list ->
+ val prepare_clauses : bool -> thm list -> thm list ->
(thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
@@ -403,23 +403,20 @@
fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th);
(* get lemmas from claset, simpset, atpset and extra supplied rules *)
-fun get_clasimp_atp_lemmas ctxt user_thms =
+fun get_clasimp_atp_lemmas ctxt =
let val included_thms =
- if include_all
- then (tap (fn ths => Output.debug
- (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
- (name_thm_pairs ctxt))
- else
- let val atpset_thms =
- if include_atpset then ResAxioms.atpset_rules_of ctxt
- else []
- val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms)
- in atpset_thms end
- val user_rules = filter check_named
- (map ResAxioms.pairname
- (if null user_thms then whitelist else user_thms))
+ if include_all
+ then (tap (fn ths => Output.debug
+ (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
+ (name_thm_pairs ctxt))
+ else
+ let val atpset_thms =
+ if include_atpset then ResAxioms.atpset_rules_of ctxt
+ else []
+ val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms)
+ in atpset_thms end
in
- (filter check_named included_thms, user_rules)
+ filter check_named included_thms
end;
(***************************************************************)
@@ -521,19 +518,20 @@
fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
let
val thy = ProofContext.theory_of ctxt
- val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
+ val included_thms = get_clasimp_atp_lemmas ctxt
val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy (isFO thy goal_cls)
|> remove_unwanted_clauses
- val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
- (*clauses relevant to goal gl*)
in
- white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
+ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
end;
(* prepare and count clauses before writing *)
-fun prepare_clauses dfg goal_cls axcls thy =
+fun prepare_clauses dfg goal_cls chain_ths axcls thy =
let
+ val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
+ val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
+ val axcls = white_cls @ axcls
val ccls = subtract_cls goal_cls axcls
val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
val ccltms = map prop_of ccls