--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue May 28 08:52:41 2013 +0200
@@ -454,7 +454,7 @@
Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover_name
val is_appropriate_prop =
Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt prover_name
- val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal i ctxt
+ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
val time_limit =
(case hard_timeout of
NONE => I