changeset 52643 | 34c29356930e |
parent 52555 | 6811291d1869 |
child 52908 | 3461985dcbc3 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Jul 13 12:39:45 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Jul 13 13:25:42 2013 +0200 @@ -140,9 +140,7 @@ state |> outcome_code = someN ? Proof.goal_message (fn () => - [Pretty.str "", - Pretty.mark Markup.intensify (Pretty.str (message ()))] - |> Pretty.chunks)) + Pretty.mark Markup.information (Pretty.str (message ())))) end else if blocking then let