src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

       val print = if mode = Normal then Output.urgent_message else K ()
       val state =
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
       val {facts = chained, goal, ...} = Proof.goal state
-      val ((_, hyp_ts, concl_t), _) = strip_subgoal goal i ctxt
+      val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
       val ho_atp = exists (is_ho_atp ctxt) provers
       val reserved = reserved_isar_keyword_table ()
       val css = clasimpset_rule_table_of ctxt
       val all_facts =
         nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts