# HG changeset patch
# User blanchet
# Date 1288250997 -7200
# Node ID 9f001f7e6c0c90c5e467df2f95a5fa2f665d3b4b
# Parent  cd6d2b0a40962dbee55e62eb6938a093ccddd4cd
clear identification

diff -r cd6d2b0a4096 -r 9f001f7e6c0c src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Oct 27 19:14:33 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Oct 28 09:29:57 2010 +0200
@@ -629,7 +629,7 @@
       in
         (pprint (Pretty.chunks
              [Pretty.blk (0,
-                  (pstrs ("Nitpick found a" ^
+                  (pstrs ((if auto then "Auto " else "") ^ "Nitpick found a" ^
                           (if not genuine then " potential "
                            else if genuine_means_genuine then " "
                            else " quasi genuine ") ^ das_wort_model) @