src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

                 play_one_line_proof mode debug verbose preplay_timeout
                     used_pairs state subgoal (hd reconstrs) reconstrs
               end,
            fn preplay =>
               let
+                val _ =
+                  if verbose then
+                    Output.urgent_message "Generating proof text..."
+                  else
+                    ()
                 val isar_params =
                   (debug, verbose, isar_shrinkage, pool, fact_names, sym_tab,
                    atp_proof, goal)
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,