diff -r da20e00050ab -r 9ed32b8a03a9 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Doc/antiquote_setup.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -40,10 +40,10 @@
     (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
     (fn ctxt =>
       map (fn (thm, name) =>
-        Output.output
+        Latex.output_
           (Document_Antiquotation.format ctxt
             (Document_Antiquotation.delimit ctxt (Document_Output.pretty_thm ctxt thm))) ^
-        enclose "\\rulename{" "}" (Output.output name))
+        enclose "\\rulename{" "}" (Latex.output_ name))
       #> space_implode "\\par\\smallskip%\n"
       #> Latex.string
       #> Document_Output.isabelle ctxt));
@@ -87,7 +87,7 @@
           if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
         val latex =
           idx ^
-          (Output.output name
+          (Latex.output_ name
             |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
             |> hyper o enclose "\\mbox{\\isa{" "}}");
       in Latex.string latex end);