src/Pure/Syntax/parser.ML
changeset 6165 a7d74bf9da52
parent 4913 44c6f462c8fa
child 6844 3909657a7da6
--- 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);