tuned message;
authorwenzelm
Sun, 29 Nov 2009 17:14:24 +0100
changeset 33919 3711139cffc3
parent 33918 5945e023bab7
child 33920 d4d430dfabc6
tuned message;
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)))));