--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 24 16:43:37 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 ctxt goal i
+ val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal i ctxt
val time_limit =
(case hard_timeout of
NONE => I