# HG changeset patch
# User wenzelm
# Date 1636829244 -3600
# Node ID 6504e9b0992614a48238b8c1780e678705885cd6
# Parent  5fca489a6ac1f5795ce424d649b0de9beeee6d47
clarified signature: more privacy;

diff -r 5fca489a6ac1 -r 6504e9b09926 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Nov 13 17:26:35 2021 +0100
+++ b/src/Pure/Thy/latex.ML	Sat Nov 13 19:47:24 2021 +0100
@@ -11,7 +11,6 @@
   val string: string -> text
   val block: text -> XML.tree
   val enclose_text: string -> string -> text -> text
-  val latex_text: text -> text
   val output_text: text -> string
   val output_name: string -> string
   val output_ascii: string -> string
@@ -55,13 +54,14 @@
 
 fun block body = XML.Elem (Markup.document_latex, body);
 
-fun latex_text text =
-  text |> maps
-    (fn XML.Elem ((name, _), body) =>
-          if name = Markup.document_latexN then latex_text body else []
-      | t => [t]);
-
-val output_text = XML.content_of o latex_text;
+val output_text =
+  let
+    fun document_latex text =
+      text |> maps
+        (fn XML.Elem ((name, _), body) =>
+              if name = Markup.document_latexN then document_latex body else []
+          | t => [t])
+  in XML.content_of o document_latex end;
 
 fun enclose_text bg en body = string bg @ body @ string en;