# HG changeset patch
# User wenzelm
# Date 1668373159 -3600
# Node ID b67c9ed2c810b90d8989794a1b32cea735d6cd69
# Parent  ca88e5496553816754f9aba2e07d85802e65f31b
tuned output;

diff -r ca88e5496553 -r b67c9ed2c810 src/Pure/Tools/prismjs.ML
--- a/src/Pure/Tools/prismjs.ML	Sun Nov 13 21:31:45 2022 +0100
+++ b/src/Pure/Tools/prismjs.ML	Sun Nov 13 21:59:19 2022 +0100
@@ -50,6 +50,8 @@
 
 end;
 
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o language_name);
+
 
 (* tokenize *)