proper enclose_name (amending e77c5bfca9aa);
authorwenzelm
Sat, 20 Nov 2021 19:39:22 +0100
changeset 74825 9bea6244c35a
parent 74824 6424f74fd9d4
child 74826 0e4d8aa61ad7
proper enclose_name (amending e77c5bfca9aa);
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 *)