src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 49921 073d69478207
parent 49918 cf441f4a358b
child 50004 c96e8e40d789
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Oct 18 15:40:02 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Oct 18 15:41:15 2012 +0200
@@ -882,6 +882,11 @@
               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)