# HG changeset patch
# User blanchet
# Date 1455536872 -3600
# Node ID 6b01bff94d87b67111406e6cacd0d34c405cbb8f
# Parent  b42858e540bb2175a27d65962b0d560598dce446
rephrased message

diff -r b42858e540bb -r 6b01bff94d87 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 15 12:47:35 2016 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 15 12:47:52 2016 +0100
@@ -919,9 +919,8 @@
                  bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
                  finitizable_dataTs
     val _ = if skipped > 0 then
-              print_nt (fn () => "Too many scopes. Skipping " ^
-                                 string_of_int skipped ^ " scope" ^
-                                 plural_s skipped ^
+              print_nt (fn () => "Skipping " ^ string_of_int skipped ^
+                                 " scope" ^ plural_s skipped ^
                                  ". (Consider using \"mono\" or \
                                  \\"merge_type_vars\" to prevent this.)")
             else