src/HOL/Tools/Nitpick/nitpick.ML
changeset 50212 4fb06c22c5ec
parent 50201 c26369c9eda6
child 50215 97959912840a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 11:42:16 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 11:59:56 2012 +0100
     1.3 @@ -470,7 +470,7 @@
     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 ()) (Pretty.blk (0,
     1.8 +                  [Pretty.mark (Sendback.make_markup {implicit = false}) (Pretty.blk (0,
     1.9                         pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
    1.10              else
    1.11                ()