--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 13 11:13:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Apr 13 11:43:11 2010 +0200
@@ -658,9 +658,9 @@
();
if not standard andalso likely_in_struct_induct_step then
print "The existence of a nonstandard model suggests that the \
- \induction hypothesis is not general enough or perhaps \
- \even wrong. See the \"Inductive Properties\" section of \
- \the Nitpick manual for details (\"isabelle doc nitpick\")."
+ \induction hypothesis is not general enough or may even be \
+ \wrong. See the Nitpick manual's \"Inductive Properties\" \
+ \section for details (\"isabelle doc nitpick\")."
else
();
if has_syntactic_sorts orig_t then