author | blanchet |
Thu, 21 Feb 2013 16:36:19 +0100 | |
changeset 51232 | 1f614b4eb367 |
parent 51231 | 67882f99274e |
child 51237 | 22ba938ab10f |
--- 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 =