src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML

 
     val (preplay, message, message_tail) =
       (case outcome of
         NONE =>
         (Lazy.lazy (fn () =>
-           play_one_line_proof mode verbose preplay_timeout used_named_facts state subgoal
-             SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
+           play_one_line_proof mode preplay_timeout used_named_facts state subgoal SMT2_Method
+             (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
          fn preplay =>
             let
+              val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
+
               fun isar_params () =
                 (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
                  goal)
 
               val one_line_params =