changeset 49358 | 0fa351b1bd14 |
parent 48798 | 9152e66f98da |
child 49914 | 23e36a4d28f1 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Sep 14 17:37:19 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Sep 14 18:12:41 2012 +0200 @@ -137,7 +137,7 @@ |> outcome_code = someN ? Proof.goal_message (fn () => [Pretty.str "", - Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))] + Pretty.mark Isabelle_Markup.intensify (Pretty.str (message ()))] |> Pretty.chunks)) end else if blocking then