# HG changeset patch
# User blanchet
# Date 1361460979 -3600
# Node ID 1f614b4eb36796f363f1517e8b7aa5fee44fc88e
# Parent  67882f99274e2d2ed598e83ec5e5186b2e676624
tuned misleading message

diff -r 67882f99274e -r 1f614b4eb367 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 21 15:10:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 21 16:36:19 2013 +0100
@@ -936,7 +936,7 @@
               let
                 val _ =
                   if verbose then
-                    Output.urgent_message "Generating structured proof..."
+                    Output.urgent_message "Generating proof text..."
                   else
                     ()
                 val isar_params =