src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
     val atp_mode =
       if Config.get ctxt completish then Sledgehammer_Completish
       else Sledgehammer
-    val ((_, hyp_ts, concl_t), ctxt') = strip_subgoal goal subgoal ctxt
+    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
     val (dest_dir, problem_prefix) =
       if overlord then overlord_file_location_of_prover name
       else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
     val problem_file_name =
       Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^