ambig msg: warning again;

--- 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;