changeset 50201 | c26369c9eda6 |
parent 49914 | 23e36a4d28f1 |
child 50557 | 31313171deb5 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Nov 25 18:50:13 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun Nov 25 19:49:24 2012 +0100 @@ -137,7 +137,7 @@ |> outcome_code = someN ? Proof.goal_message (fn () => [Pretty.str "", - Pretty.mark Isabelle_Markup.intensify (Pretty.str (message ()))] + Pretty.mark Markup.intensify (Pretty.str (message ()))] |> Pretty.chunks)) end else if blocking then