src/HOL/Tools/Nitpick/nitpick.ML
changeset 50215 97959912840a
parent 50212 4fb06c22c5ec
child 50450 358b6020f8b6
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 14:43:28 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 16:16:47 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}) (Pretty.blk (0,
     1.8 +                  [Pretty.mark (Sendback.make_markup {implicit = false, properties = []})
     1.9 +                    (Pretty.blk (0,
    1.10                         pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
    1.11              else
    1.12                ()