changeset 3739 | 13f7107676a0 |
parent 3526 | df4d0dad2b4e |
child 3779 | ce8594f7e0c6 |
--- 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);