diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Mon Nov 15 17:26:31 2021 +0100
@@ -484,13 +484,13 @@
 
 fun isabelle ctxt body =
   if Config.get ctxt Document_Antiquotation.thy_output_display
-  then Latex.environment_text "isabelle" body
-  else XML.enclose "\\isa{" "}" body;
+  then Latex.environment "isabelle" body
+  else Latex.macro "isa" body;
 
 fun isabelle_typewriter ctxt body =
   if Config.get ctxt Document_Antiquotation.thy_output_display
-  then Latex.environment_text "isabellett" body
-  else XML.enclose "\\isatt{" "}" body;
+  then Latex.environment "isabellett" body
+  else Latex.macro "isatt" body;
 
 fun typewriter ctxt s =
   isabelle_typewriter ctxt (Latex.string (Latex.output_ascii s));