diff -r 47f565849e71 -r d2522bb4db1b src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Sun Nov 14 15:42:38 2021 +0100
+++ b/src/Pure/Tools/rail.ML	Sun Nov 14 17:46:41 2021 +0100
@@ -341,47 +341,51 @@
   let
     val output_antiq =
       Antiquote.Antiq #>
-      Document_Antiquotation.evaluate Latex.symbols ctxt #>
-      Latex.output_text;
+      Document_Antiquotation.evaluate Latex.symbols ctxt;
     fun output_text b s =
       Output.output s
       |> b ? enclose "\\isakeyword{" "}"
-      |> enclose "\\isa{" "}";
+      |> enclose "\\isa{" "}"
+      |> Latex.string;
 
     fun output_cat c (Cat (_, rails)) = outputs c rails
     and outputs c [rail] = output c rail
-      | outputs _ rails = implode (map (output "") rails)
-    and output _ (Bar []) = ""
+      | outputs _ rails = maps (output "") rails
+    and output _ (Bar []) = []
       | output c (Bar [cat]) = output_cat c cat
       | output _ (Bar (cat :: cats)) =
-          "\\rail@bar\n" ^ output_cat "" cat ^
-          implode (map (fn Cat (y, rails) =>
-              "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
-          "\\rail@endbar\n"
+          Latex.string ("\\rail@bar\n") @ output_cat "" cat @
+          maps (fn Cat (y, rails) =>
+            Latex.string ("\\rail@nextbar{" ^ string_of_int y ^ "}\n") @ outputs "" rails) cats @
+          Latex.string "\\rail@endbar\n"
       | output c (Plus (cat, Cat (y, rails))) =
-          "\\rail@plus\n" ^ output_cat c cat ^
-          "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
-          "\\rail@endplus\n"
-      | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
-      | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text false s ^ "}[]\n"
-      | output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n"
+          Latex.string "\\rail@plus\n" @ output_cat c cat @
+          Latex.string ("\\rail@nextplus{" ^ string_of_int y ^ "}\n") @ outputs "c" rails @
+          Latex.string "\\rail@endplus\n"
+      | output _ (Newline y) = Latex.string ("\\rail@cr{" ^ string_of_int y ^ "}\n")
+      | output c (Nonterminal s) =
+          Latex.string ("\\rail@" ^ c ^ "nont{") @ output_text false s @ Latex.string "}[]\n"
+      | output c (Terminal (b, s)) =
+          Latex.string ("\\rail@" ^ c ^ "term{") @ output_text b s @ Latex.string "}[]\n"
       | output c (Antiquote (b, a)) =
-          "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n";
+          Latex.string ("\\rail@" ^ c ^ (if b then "term{" else "nont{")) @
+          Latex.output (output_antiq a) @
+          Latex.string "}[]\n";
 
     fun output_rule (name, rail) =
       let
         val (rail', y') = vertical_range rail 0;
         val out_name =
           (case name of
-            Antiquote.Text "" => ""
+            Antiquote.Text "" => []
           | Antiquote.Text s => output_text false s
           | Antiquote.Antiq a => output_antiq a);
       in
-        "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
-        output "" rail' ^
-        "\\rail@end\n"
+        Latex.string ("\\rail@begin{" ^ string_of_int y' ^ "}{") @ out_name @ Latex.string "}\n" @
+        output "" rail' @
+        Latex.string "\\rail@end\n"
       end;
-  in Latex.environment_text "railoutput" (Latex.string (implode (map output_rule rules))) end;
+  in Latex.environment_text "railoutput" (maps output_rule rules) end;
 
 val _ = Theory.setup
   (Document_Output.antiquotation_raw_embedded \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)