diff -r ce40cee07fbc -r 670cbec816b9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -208,7 +208,7 @@
                  (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
                   goal)
 
-               val one_line_params = (preplay, proof_banner mode name, subgoal, subgoal_count)
+               val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
                val num_chained = length (#facts (Proof.goal state))
              in
                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained