src/HOL/Tools/Nitpick/nitpick.ML
changeset 45666 d83797ef0d2d
parent 44395 d39aedffba08
child 46086 096697aec8a7
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 28 20:39:08 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 28 22:05:32 2011 +0100
     1.3 @@ -239,7 +239,7 @@
     1.4        if mode = Auto_Try then
     1.5          Unsynchronized.change state_ref o Proof.goal_message o K
     1.6          o Pretty.chunks o cons (Pretty.str "") o single
     1.7 -        o Pretty.mark Markup.hilite
     1.8 +        o Pretty.mark Isabelle_Markup.hilite
     1.9        else
    1.10          (fn s => (Output.urgent_message s; if debug then tracing s else ()))
    1.11          o Pretty.string_of
    1.12 @@ -459,7 +459,7 @@
    1.13                pprint_n (fn () => Pretty.blk (0,
    1.14                    pstrs "Hint: To check that the induction hypothesis is \
    1.15                          \general enough, try this command: " @
    1.16 -                  [Pretty.mark Markup.sendback (Pretty.blk (0,
    1.17 +                  [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0,
    1.18                         pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
    1.19              else
    1.20                ()