# HG changeset patch
# User wenzelm
# Date 1259511264 -3600
# Node ID 3711139cffc34d3d8a948dd2bd8ebd7a965262c6
# Parent  5945e023bab7f1447b0e1e9e3f1cc675dc9cf477
tuned message;

diff -r 5945e023bab7 -r 3711139cffc3 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Nov 29 17:13:27 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sun Nov 29 17:14:24 2009 +0100
@@ -496,7 +496,7 @@
     else if ! ambiguity_is_error then error (ambiguity_msg pos)
     else
       (warning (cat_lines
-        (("Ambiguous input " ^ Position.str_of pos ^
+        (("Ambiguous input" ^ Position.str_of pos ^
           "\nproduces " ^ string_of_int len ^ " parse trees" ^
           (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
           map show_pt (Library.take (limit, pts)))));