diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -491,6 +491,6 @@
 
 val _ =
   ML_system_pp (fn _ => fn _ =>
-    Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
+    Pretty.to_ML o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
 
 end;