# HG changeset patch
# User wenzelm
# Date 875535078 -7200
# Node ID 13f7107676a0ee97f6f9efc2806e43e04525c0d0
# Parent  27f7473d029aef385a8f78a480ff62c800d09eed
improved warning;

diff -r 27f7473d029a -r 13f7107676a0 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Sep 29 14:10:52 1997 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Sep 29 14:11:18 1997 +0200
@@ -353,7 +353,8 @@
     val chars = SymbolFont.read_charnames (explode str);
     val pts = parse gram root' (tokenize lexicon xids chars);
 
-    fun show_pt pt = warning (str_of_ast (pt_to_ast (K None) pt));
+    fun show_pt pt =
+      warning (Pretty.string_of (pretty_ast (pt_to_ast (K None) pt)));
   in
     if length pts > ! ambiguity_level then
       (warning ("Ambiguous input " ^ quote str);