# HG changeset patch
# User wenzelm
# Date 1120250196 -7200
# Node ID 4748b1adad9cb9fdc991c490945be7cd939e1ab7
# Parent  fdb4992cf1d2d233605a958da14d73dbfc437f45
ambig msg: warning again;

diff -r fdb4992cf1d2 -r 4748b1adad9c src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Jul 01 22:35:41 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Jul 01 22:36:36 2005 +0200
@@ -371,7 +371,7 @@
       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).");
-         List.app (tracing o show_pt) pts));
+         List.app (warning o show_pt) pts));
     SynTrans.pts_to_asts thy (lookup_tr parse_ast_trtab) pts
   end;