diff -r da20e00050ab -r 9ed32b8a03a9 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/Tools/rail.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -332,7 +332,7 @@
       Antiquote.Antiq #>
       Document_Antiquotation.evaluate Latex.symbols ctxt;
     fun output_text b s =
-      Latex.string (Output.output s)
+      Latex.string (Latex.output_ s)
       |> b ? Latex.macro "isakeyword"
       |> Latex.macro "isa";