--- 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,
--- 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 ()