--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 30 08:53:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 30 09:41:59 2010 +0200
@@ -216,10 +216,9 @@
relevance_thresholds, max_relevant, theory_relevant, isar_proof,
isar_shrink_factor, timeout, ...} : params)
minimize_command
- ({subgoal, goal, relevance_override, axioms} : problem) =
+ ({subgoal, goal = (ctxt, (chained_ths, th)), relevance_override,
+ axioms} : problem) =
let
- val (ctxt, (_, th)) = goal;
- val thy = ProofContext.theory_of ctxt
val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
val print = priority
@@ -230,10 +229,10 @@
case axioms of
SOME axioms => axioms
| NONE =>
- (relevant_facts full_types relevance_thresholds
+ (relevant_facts ctxt full_types relevance_thresholds
(the_default default_max_relevant max_relevant)
(the_default default_theory_relevant theory_relevant)
- relevance_override goal hyp_ts concl_t
+ relevance_override chained_ths hyp_ts concl_t
|> tap ((fn n => print_v (fn () =>
"Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
" for " ^ quote atp_name ^ ".")) o length))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 30 08:53:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 30 09:41:59 2010 +0200
@@ -17,9 +17,8 @@
Proof.context -> unit Symtab.table -> thm list -> Facts.ref
-> ((string * locality) * thm) list
val relevant_facts :
- bool -> real * real -> int -> bool -> relevance_override
- -> Proof.context * (thm list * 'a) -> term list -> term
- -> ((string * locality) * thm) list
+ Proof.context -> bool -> real * real -> int -> bool -> relevance_override
+ -> thm list -> term list -> term -> ((string * locality) * thm) list
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -672,9 +671,9 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun relevant_facts full_types (threshold0, threshold1) max_relevant
+fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
theory_relevant (relevance_override as {add, del, only})
- (ctxt, (chained_ths, _)) hyp_ts concl_t =
+ chained_ths hyp_ts concl_t =
let
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
1.0 / Real.fromInt (max_relevant + 1))