src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

         (outcome_code,
          state
          |> outcome_code = someN
             ? Proof.goal_message (fn () =>
                   [Pretty.str "",
-                   Pretty.mark Markup.hilite (Pretty.str (message ()))]
+                   Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))]
                   |> Pretty.chunks))
       end
     else if blocking then
       let
         val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()