1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 27 10:30:07 2011 +0200
1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 27 10:30:07 2011 +0200
1.3 @@ -390,7 +390,7 @@
1.4 val relevance_fudge =
1.5 Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
1.6 val relevance_override = {add = [], del = [], only = false}
1.7 - val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
1.8 + val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal ctxt goal i
1.9 val time_limit =
1.10 (case hard_timeout of
1.11 NONE => I