# 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 =