diff -r 056ec8201667 -r 2281f33e8da6 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue May 28 08:52:41 2013 +0200
@@ -124,8 +124,7 @@
            extract_relevance_fudge args
                (Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover)
          val subgoal = 1
-         val ((_, hyp_ts, concl_t), ctxt) =
-           ATP_Util.strip_subgoal goal subgoal ctxt
+         val (_, hyp_ts, concl_t) = 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