# HG changeset patch
# User wenzelm
# Date 1637433562 -3600
# Node ID 9bea6244c35acd27a3d4f02fe4786358f09191f5
# Parent  6424f74fd9d4cec9202a34d7e078baf69f0e01a6
proper enclose_name (amending e77c5bfca9aa);

diff -r 6424f74fd9d4 -r 9bea6244c35a src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Nov 20 18:58:23 2021 +0100
+++ b/src/Pure/Thy/latex.ML	Sat Nov 20 19:39:22 2021 +0100
@@ -201,7 +201,7 @@
 val begin_delim = enclose_name "%\n\\isadelim" "\n";
 val end_delim = enclose_name "%\n\\endisadelim" "\n";
 val begin_tag = enclose_name "%\n\\isatag" "\n";
-fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
+fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose_name "{\\isafold" "}%\n" tg;
 
 
 (* theory presentation *)