src/Pure/Syntax/syntax.ML

     fun show_pt pt =
       Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts thy (K NONE) [pt])));
   in
     conditional (length pts > ! ambiguity_level) (fn () =>
       if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
-      else warning (cat_lines ("Ambiguous input " ^ quote str ::
-        "produces the following parse trees:" :: map show_pt pts)));
+      else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
+          "produces " ^ string_of_int (length pts) ^ " parse trees (see trace).");
+         List.app (tracing o show_pt) pts));
     SynTrans.pts_to_asts thy (lookup_tr parse_ast_trtab) pts
   end;
 
 
 (* read *)