tuned msg;
authorwenzelm
Wed, 06 Jul 2005 10:41:50 +0200
changeset 16716 57fd954ee326
parent 16715 ecca9fd2754f
child 16717 710a7a7a2b65
tuned msg;
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;