# HG changeset patch
# User wenzelm
# Date 1450084459 -3600
# Node ID 1803599838a66ebbfedb3f0c3e59812f9014ede5
# Parent  00b70452dc7fc2cb1125061ac25b94d035a59320
tuned message;

diff -r 00b70452dc7f -r 1803599838a6 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Dec 13 22:33:05 2015 +0100
+++ b/src/Pure/Isar/method.ML	Mon Dec 14 10:14:19 2015 +0100
@@ -741,7 +741,7 @@
       | bad =>
           if detect_closure_state st then NONE
           else
-            SOME (fn () => ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
+            SOME (fn () => ("Excessive case name(s): " ^ commas_quote (map Token.content_of bad) ^
               Position.here (Position.set_range (Token.range_of bad)))))
       |> (fn SOME msg => Seq.single (Seq.Error msg)
            | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st)))))