src/Pure/Thy/latex.scala

--- a/src/Pure/Thy/latex.scala	Sun Nov 14 21:52:13 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Mon Nov 15 11:38:14 2021 +0100
@@ -77,8 +77,8 @@
   {
     def latex_output(latex_text: Text): String = apply(latex_text)
 
-    def latex_macro(name: String, arg: Text): Text =
-      XML.string("\\" + name + "{") ::: arg ::: XML.string("}")
+    def latex_macro(name: String, body: Text): Text =
+      XML.enclose("\\" + name + "{", "}", body)
 
     def index_item(item: Index_Item.Value): String =
     {