src/HOL/Tools/Nitpick/nitpick.ML
changeset 50450 358b6020f8b6
parent 50215 97959912840a
child 50487 9486641e691b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 10 10:41:29 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 10 13:52:33 2012 +0100
     1.3 @@ -470,7 +470,8 @@
     1.4                pprint_nt (fn () => Pretty.blk (0,
     1.5                    pstrs "Hint: To check that the induction hypothesis is \
     1.6                          \general enough, try this command: " @
     1.7 -                  [Pretty.mark (Sendback.make_markup {implicit = false, properties = []})
     1.8 +                  [Pretty.mark
     1.9 +                    (Active.make_markup Markup.sendbackN {implicit = false, properties = []})
    1.10                      (Pretty.blk (0,
    1.11                         pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
    1.12              else