# HG changeset patch
# User oheimb
# Date 917626300 -3600
# Node ID a7d74bf9da52e3a427e02878a7214fecd18c3256
# Parent  a0e9501d56f84d760f80bff2cfd3792d4416a2ad
corrected output of symbols for several (probably not all) relevant functions

diff -r a0e9501d56f8 -r a7d74bf9da52 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Jan 29 17:10:26 1999 +0100
+++ b/src/Pure/Syntax/parser.ML	Fri Jan 29 17:11:40 1999 +0100
@@ -792,7 +792,8 @@
       if null toks then Pretty.str "Inner syntax error: unexpected end of input"
       else
         Pretty.block (Pretty.str "Inner syntax error at: \"" ::
-          Pretty.breaks (map (Pretty.str o str_of_token) (rev (tl (rev toks)))) @
+          Pretty.breaks (map (Pretty.str o Symbol.output o str_of_token)
+		 (rev (tl (rev toks)))) @
           [Pretty.str "\""]);
     val expected =
       Pretty.strs ("Expected tokens: " :: map (quote o str_of_token) allowed);