--- a/src/HOL/TPTP/sledgehammer_tactics.ML Tue May 28 08:36:12 2013 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Tue May 28 08:52:41 2013 +0200
@@ -32,7 +32,7 @@
val name = hd provers
val prover = get_prover ctxt mode name
val default_max_facts = default_max_facts_of_prover ctxt slice name
- val ((_, hyp_ts, concl_t), _) = ATP_Util.strip_subgoal goal i ctxt
+ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
val ho_atp = exists (is_ho_atp ctxt) provers
val reserved = reserved_isar_keyword_table ()
val css_table = clasimpset_rule_table_of ctxt