--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jan 02 10:41:53 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jan 02 10:54:36 2013 +0100
@@ -102,7 +102,7 @@
|> (fn {outcome, preplay, message, message_tail, ...} =>
(if outcome = SOME ATP_Proof.TimedOut then timeoutN
else if is_some outcome then noneN
- else someN, fn () => message (preplay ()) ^ message_tail))
+ else someN, fn () => message (Lazy.force preplay) ^ message_tail))
fun go () =
let
val (outcome_code, message) =