# HG changeset patch
# User wenzelm
# Date 1361467648 -3600
# Node ID 22ba938ab10f15463cc591c4c96e027185d7145a
# Parent  1f614b4eb36796f363f1517e8b7aa5fee44fc88e# Parent  f301ad90c48b87670429d180a2b42bae1566a86d
merged

diff -r f301ad90c48b -r 22ba938ab10f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 21 18:21:40 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 21 18:27:28 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 =