src/Pure/Thy/latex.ML

--- a/src/Pure/Thy/latex.ML	Sun Dec 05 12:50:36 2021 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Dec 05 15:54:46 2021 +0100
@@ -14,7 +14,6 @@
   val macro0: string -> text
   val macro: string -> text -> text
   val environment: string -> text -> text
-  val enclose_text: string -> string -> text -> text
   val output_name: string -> string
   val output_ascii: string -> string
   val output_ascii_breakable: string -> string -> string
@@ -57,8 +56,6 @@
 fun macro name body = [XML.Elem (Markup.latex_macro name, body)];
 fun environment name body = [XML.Elem (Markup.latex_environment name, body)];
 
-fun enclose_text bg en body = string bg @ body @ string en;
-
 
 (* output name for LaTeX macros *)
 
@@ -195,12 +192,12 @@
 (* theory presentation *)
 
 fun environment_text name =
-  enclose_text
+  XML.enclose
     ("%\n\\begin{" ^ output_name name ^ "}%\n")
     ("%\n\\end{" ^ output_name name ^ "}");
 
 fun isabelle_body name =
-  enclose_text
+  XML.enclose
    ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
    "%\n\\end{isabellebody}%\n";