--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 26 14:43:28 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 26 16:16:47 2012 +0100
@@ -470,7 +470,8 @@
pprint_nt (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
\general enough, try this command: " @
- [Pretty.mark (Sendback.make_markup {implicit = false}) (Pretty.blk (0,
+ [Pretty.mark (Sendback.make_markup {implicit = false, properties = []})
+ (Pretty.blk (0,
pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
else
()