src/Pure/Syntax/syntax.ML

     val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
     val root' = if root mem logtypes then SynExt.logic else root;
     val chars = Symbol.explode str;
     val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
 
-    fun show_pt pt =
-      warning (Symbol.output (Pretty.string_of 
-		(Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt))));
+    fun show_pt pt = warning (Pretty.string_of 
+			(Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
   in
     if length pts > ! ambiguity_level then
-      (warning ("Ambiguous input " ^ quote (Symbol.output str));
+      (warning ("Ambiguous input " ^ quote str);
        warning "produces the following parse trees:";
        seq show_pt pts)
     else ();
     map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts
   end;