--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Dec 19 17:24:17 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Dec 19 17:52:58 2013 +0100
@@ -464,8 +464,8 @@
fun failed failure =
({outcome = SOME failure, used_facts = [], used_from = [],
run_time = Time.zeroTime,
- preplay = Lazy.value (Sledgehammer_Reconstructor.Play_Failed
- Sledgehammer_Provers.plain_metis),
+ preplay = Lazy.value (Sledgehammer_Provers.plain_metis,
+ Sledgehammer_Reconstructor.Play_Failed),
message = K "", message_tail = ""}, ~1)
val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
: Sledgehammer_Provers.prover_result,