src/Pure/Thy/document_output.ML
changeset 74790 3ce6fb9db485
parent 74789 a5c23da73fca
child 74823 d6ce4ce20422
--- 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));