1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 06 20:36:34 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 06 20:36:34 2011 +0200
     1.3 @@ -398,7 +398,7 @@
     1.4        | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     1.5      fun failed failure =
     1.6        ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
     1.7 -        preplay = K ATP_Reconstruct.Failed_to_Play,
     1.8 +        preplay = K (ATP_Reconstruct.Failed_to_Play ATP_Reconstruct.Metis),
     1.9          message = K ""}, ~1)
    1.10      val ({outcome, used_facts, run_time_in_msecs, preplay, message}
    1.11           : Sledgehammer_Provers.prover_result,