diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Mon Nov 15 11:38:14 2021 +0100 +++ b/src/Pure/Tools/rail.ML Mon Nov 15 17:26:31 2021 +0100 @@ -343,10 +343,9 @@ Antiquote.Antiq #> Document_Antiquotation.evaluate Latex.symbols ctxt; fun output_text b s = - Output.output s - |> b ? enclose "\\isakeyword{" "}" - |> enclose "\\isa{" "}" - |> Latex.string; + Latex.string (Output.output s) + |> b ? Latex.macro "isakeyword" + |> Latex.macro "isa"; fun output_cat c (Cat (_, rails)) = outputs c rails and outputs c [rail] = output c rail