src/Pure/Syntax/syntax.ML
changeset 3739 13f7107676a0
parent 3526 df4d0dad2b4e
child 3779 ce8594f7e0c6
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Sep 29 14:10:52 1997 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Sep 29 14:11:18 1997 +0200
     1.3 @@ -353,7 +353,8 @@
     1.4      val chars = SymbolFont.read_charnames (explode str);
     1.5      val pts = parse gram root' (tokenize lexicon xids chars);
     1.6  
     1.7 -    fun show_pt pt = warning (str_of_ast (pt_to_ast (K None) pt));
     1.8 +    fun show_pt pt =
     1.9 +      warning (Pretty.string_of (pretty_ast (pt_to_ast (K None) pt)));
    1.10    in
    1.11      if length pts > ! ambiguity_level then
    1.12        (warning ("Ambiguous input " ^ quote str);