--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 02 15:10:18 2014 +0200
@@ -287,7 +287,7 @@
|> (fn accum as (output, _) =>
(accum,
extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
- |>> atp_proof_of_tstplike_proof atp_problem
+ |>> atp_proof_of_tstplike_proof name atp_problem
handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
val outcome =