src/Pure/Tools/rail.ML
changeset 74790 3ce6fb9db485
parent 74784 d2522bb4db1b
child 74882 947bb3e09a88
--- 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