# HG changeset patch
# User wenzelm
# Date 1120639310 -7200
# Node ID 57fd954ee326561787163dc956df42cb3dc0cf62
# Parent  ecca9fd2754f644dee761745f762872f9ed6c533
tuned msg;

diff -r ecca9fd2754f -r 57fd954ee326 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Jul 06 10:41:49 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Jul 06 10:41:50 2005 +0200
@@ -370,7 +370,7 @@
     conditional (length pts > ! ambiguity_level) (fn () =>
       if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
       else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
-          "produces " ^ string_of_int (length pts) ^ " parse trees (see trace).");
+          "produces " ^ string_of_int (length pts) ^ " parse trees.");
          List.app (warning o show_pt) pts));
     SynTrans.pts_to_asts thy (lookup_tr parse_ast_trtab) pts
   end;