# HG changeset patch
# User blanchet
# Date 1283154119 -7200
# Node ID 6e47e54214b81edfd32e4cbe64135077ed327c7d
# Parent  fd803530e8a0a399dacde2799cb426d48e33d20d
remove needless parameter

diff -r fd803530e8a0 -r 6e47e54214b8 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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))
diff -r fd803530e8a0 -r 6e47e54214b8 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- 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))