--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri May 24 16:43:37 2013 +0200
@@ -124,7 +124,8 @@
extract_relevance_fudge args
(Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover)
val subgoal = 1
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
+ val ((_, hyp_ts, concl_t), ctxt) =
+ ATP_Util.strip_subgoal goal subgoal ctxt
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt