# HG changeset patch
# User wenzelm
# Date 889456273 -3600
# Node ID fc5687450acc4ebed19b85cb0bf50720a866ebd5
# Parent  44e33cfdbb46f17abb13c6b6199d0b1f4b1ff967
Symbol.output;

diff -r 44e33cfdbb46 -r fc5687450acc src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Mon Mar 09 16:10:57 1998 +0100
+++ b/src/Pure/Syntax/printer.ML	Mon Mar 09 16:11:13 1998 +0100
@@ -213,11 +213,11 @@
           (if is_terminal s then max_pri else p);
 
         fun xsyms_to_syms (Delim s :: xsyms) =
-              apfst (cons_str s) (xsyms_to_syms xsyms)
+              apfst (cons_str (Symbol.output s)) (xsyms_to_syms xsyms)
           | xsyms_to_syms (Argument s_p :: xsyms) =
               apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
           | xsyms_to_syms (Space s :: xsyms) =
-              apfst (cons_str s) (xsyms_to_syms xsyms)
+              apfst (cons_str (Symbol.output s)) (xsyms_to_syms xsyms)
           | xsyms_to_syms (Bg i :: xsyms) =
               let
                 val (bsyms, xsyms') = xsyms_to_syms xsyms;