diff -r a1fa82431576 -r d6ce4ce20422 src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Sat Nov 20 13:53:34 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Sat Nov 20 18:15:09 2021 +0100
@@ -200,11 +200,10 @@
   (case tok of
     Ignore => []
   | Token tok => output_token ctxt tok
-  | Heading (cmd, source) =>
-      XML.enclose ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
-        (output_document ctxt {markdown = false} source)
-  | Body (cmd, source) =>
-      Latex.environment_text ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)
+  | Heading (kind, source) =>
+      [XML.Elem (Markup.latex_heading kind, output_document ctxt {markdown = false} source)]
+  | Body (kind, source) =>
+      [XML.Elem (Markup.latex_body kind, output_document ctxt {markdown = true} source)]
   | Raw source =>
       Latex.string "%\n" @ output_document ctxt {markdown = true} source @ Latex.string "\n");