diff -r 44bd3c094fd6 -r afbd8241797b src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Jul 16 22:24:42 1999 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Jul 16 22:25:07 1999 +0200
@@ -281,7 +281,7 @@
     val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs;
     val prmodes' = sort_strings (filter_out (equal "") prmodes);
   in
-    Pretty.writeln (pretty_strs_qs "lexicon:" (map implode (Scan.dest_lexicon lexicon)));
+    Pretty.writeln (pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon));
     Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
     Pretty.writeln (Pretty.big_list "prods:" (Parser.pretty_gram gram));
     Pretty.writeln (pretty_strs_qs "print modes:" prmodes')