src/Pure/Syntax/syntax.ML

     val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
     val root' = if root mem logtypes then logic else root;
     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);
        warning "produces the following parse trees:";
        seq show_pt pts)