Symbol.output;
authorwenzelm
Mon, 09 Mar 1998 16:11:13 +0100
changeset 4699 fc5687450acc
parent 4698 44e33cfdbb46
child 4700 20ade76722d6
Symbol.output;
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;