src/HOL/Tools/Nitpick/nitpick.ML

     val state_ref = Unsynchronized.ref state
     val pprint =
       if mode = Auto_Try then
         Unsynchronized.change state_ref o Proof.goal_message o K
         o Pretty.chunks o cons (Pretty.str "") o single
-        o Pretty.mark Markup.hilite
+        o Pretty.mark Isabelle_Markup.hilite
       else
         (fn s => (Output.urgent_message s; if debug then tracing s else ()))
         o Pretty.string_of
     fun pprint_n f = () |> mode = Normal ? pprint o f
     fun pprint_v f = () |> verbose ? pprint o f

       exists is_struct_induct_step (Proof_Context.cases_of ctxt)
     val _ = if standard andalso likely_in_struct_induct_step then
               pprint_n (fn () => Pretty.blk (0,
                   pstrs "Hint: To check that the induction hypothesis is \
                         \general enough, try this command: " @
-                  [Pretty.mark Markup.sendback (Pretty.blk (0,
+                  [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0,
                        pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
             else
               ()
 (*
     val _ = print_g "Monotonic types:"