# HG changeset patch
# User blanchet
# Date 1297354732 -3600
# Node ID 1e3a8807ebd4ca8b586cf1d9fabe8ac84e26b26a
# Parent  657712cc88474d62c4e64164ea673b7e262a100e
tuning

diff -r 657712cc8847 -r 1e3a8807ebd4 src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML	Thu Feb 10 17:17:31 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML	Thu Feb 10 17:18:52 2011 +0100
@@ -39,13 +39,6 @@
           relevance_thresholds
           (the_default default_max_relevant max_relevant) is_built_in_const
           relevance_fudge relevance_override chained_ths hyp_ts concl_t
-    (* Check for constants other than the built-in HOL constants. If none of
-       them appear (as should be the case for TPTP problems, unless "auto" or
-       "simp" already did its "magic"), we can skip the relevance filter. *)
-    val pure_goal =
-      not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
-                                      not (String.isSubstring "HOL" s))
-                        (prop_of goal))
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
        facts = map Sledgehammer_Provers.Untranslated_Fact facts,
diff -r 657712cc8847 -r 1e3a8807ebd4 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Feb 10 17:17:31 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Feb 10 17:18:52 2011 +0100
@@ -145,13 +145,11 @@
 fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt
                    silent i n state facts =
   let
-    val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
     val prover = get_prover ctxt false prover_name
     val msecs = Time.toMilliseconds timeout
     val _ = print silent (fn () => "Sledgehammer minimize: " ^
                                    quote prover_name ^ ".")
-    val {goal, ...} = Proof.goal state
     fun do_test timeout =
       test_facts params explicit_apply_opt silent prover timeout i n state
     val timer = Timer.startRealTimer ()