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