src/HOL/ex/sledgehammer_tactics.ML
changeset 43004 20e9caff1f86
parent 42944 9e620869a576
child 43021 5910dd009d0e
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Fri May 27 10:30:07 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Fri May 27 10:30:07 2011 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4      val relevance_fudge =
     1.5        Sledgehammer_Provers.relevance_fudge_for_prover ctxt 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 facts =
    1.10        Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    1.11            (the_default default_max_relevant max_relevant) (K true)