diff --git a/thys/CZH_Elementary_Categories/document/style.sty b/thys/CZH_Elementary_Categories/document/style.sty
--- a/thys/CZH_Elementary_Categories/document/style.sty
+++ b/thys/CZH_Elementary_Categories/document/style.sty
@@ -1,42 +1,42 @@
 %% toc
 
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
 %% references
 \newcommand{\partref}[1]{part~\ref{#1}}
 \newcommand{\secref}[1]{\S\ref{#1}}
 \newcommand{\chref}[1]{chapter~\ref{#1}}
 \newcommand{\Chref}[1]{Chapter~\ref{#1}}
 \newcommand{\appref}[1]{appendix~\ref{#1}}
 \newcommand{\Appref}[1]{Appendix~\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
 \newcommand{\Figref}[1]{Figure~\ref{#1}}
 
 %% Isar
 \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
 \renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
 \newcommand{\isasymdoublequote}{\texttt{\upshape"}}
 
 %% ML
 \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
 
 \renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\isadigitreset}
-\renewcommand{\endisatagML}{\endgroup}
+\def\endisatagML{\endgroup}
 
 %% math
 \newcommand{\isasymstrut}{\isamath{\mathstrut}}
 \newcommand{\isasymvartheta}{\isamath{\,\theta}}
 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
 %% global style options
 \pagestyle{headings}
 \sloppy
 
 \parindent 0pt\parskip 0.5ex
 
 \isabellestyle{literalunderscore}
 
 \railtermfont{\isabellestyle{tt}}
 \railnontermfont{\isabellestyle{literalunderscore}}
 \railnamefont{\isabellestyle{literalunderscore}}
diff --git a/thys/CZH_Foundations/document/style.sty b/thys/CZH_Foundations/document/style.sty
--- a/thys/CZH_Foundations/document/style.sty
+++ b/thys/CZH_Foundations/document/style.sty
@@ -1,42 +1,42 @@
 %% toc
 
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
 %% references
 \newcommand{\partref}[1]{part~\ref{#1}}
 \newcommand{\secref}[1]{\S\ref{#1}}
 \newcommand{\chref}[1]{chapter~\ref{#1}}
 \newcommand{\Chref}[1]{Chapter~\ref{#1}}
 \newcommand{\appref}[1]{appendix~\ref{#1}}
 \newcommand{\Appref}[1]{Appendix~\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
 \newcommand{\Figref}[1]{Figure~\ref{#1}}
 
 %% Isar
 \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
 \renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
 \newcommand{\isasymdoublequote}{\texttt{\upshape"}}
 
 %% ML
 \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
 
 \renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\isadigitreset}
-\renewcommand{\endisatagML}{\endgroup}
+\def\endisatagML{\endgroup}
 
 %% math
 \newcommand{\isasymstrut}{\isamath{\mathstrut}}
 \newcommand{\isasymvartheta}{\isamath{\,\theta}}
 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
 %% global style options
 \pagestyle{headings}
 \sloppy
 
 \parindent 0pt\parskip 0.5ex
 
 \isabellestyle{literalunderscore}
 
 \railtermfont{\isabellestyle{tt}}
 \railnontermfont{\isabellestyle{literalunderscore}}
 \railnamefont{\isabellestyle{literalunderscore}}
diff --git a/thys/CZH_Universal_Constructions/document/style.sty b/thys/CZH_Universal_Constructions/document/style.sty
--- a/thys/CZH_Universal_Constructions/document/style.sty
+++ b/thys/CZH_Universal_Constructions/document/style.sty
@@ -1,42 +1,42 @@
 %% toc
 
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
 %% references
 \newcommand{\partref}[1]{part~\ref{#1}}
 \newcommand{\secref}[1]{\S\ref{#1}}
 \newcommand{\chref}[1]{chapter~\ref{#1}}
 \newcommand{\Chref}[1]{Chapter~\ref{#1}}
 \newcommand{\appref}[1]{appendix~\ref{#1}}
 \newcommand{\Appref}[1]{Appendix~\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
 \newcommand{\Figref}[1]{Figure~\ref{#1}}
 
 %% Isar
 \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
 \renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
 \newcommand{\isasymdoublequote}{\texttt{\upshape"}}
 
 %% ML
 \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
 
 \renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\isadigitreset}
-\renewcommand{\endisatagML}{\endgroup}
+\def\endisatagML{\endgroup}
 
 %% math
 \newcommand{\isasymstrut}{\isamath{\mathstrut}}
 \newcommand{\isasymvartheta}{\isamath{\,\theta}}
 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
 %% global style options
 \pagestyle{headings}
 \sloppy
 
 \parindent 0pt\parskip 0.5ex
 
 \isabellestyle{literalunderscore}
 
 \railtermfont{\isabellestyle{tt}}
 \railnontermfont{\isabellestyle{literalunderscore}}
 \railnamefont{\isabellestyle{literalunderscore}}
diff --git a/thys/Types_To_Sets_Extension/document/style.sty b/thys/Types_To_Sets_Extension/document/style.sty
--- a/thys/Types_To_Sets_Extension/document/style.sty
+++ b/thys/Types_To_Sets_Extension/document/style.sty
@@ -1,42 +1,42 @@
 %% toc
 
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
 %% references
 \newcommand{\partref}[1]{part~\ref{#1}}
 \newcommand{\secref}[1]{\S\ref{#1}}
 \newcommand{\chref}[1]{chapter~\ref{#1}}
 \newcommand{\Chref}[1]{Chapter~\ref{#1}}
 \newcommand{\appref}[1]{appendix~\ref{#1}}
 \newcommand{\Appref}[1]{Appendix~\ref{#1}}
 \newcommand{\figref}[1]{figure~\ref{#1}}
 \newcommand{\Figref}[1]{Figure~\ref{#1}}
 
 %% Isar
 \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
 \renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
 \newcommand{\isasymdoublequote}{\texttt{\upshape"}}
 
 %% ML
 \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
 
 \renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\isadigitreset}
-\renewcommand{\endisatagML}{\endgroup}
+\def\endisatagML{\endgroup}
 
 %% math
 \newcommand{\isasymstrut}{\isamath{\mathstrut}}
 \newcommand{\isasymvartheta}{\isamath{\,\theta}}
 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
 %% global style options
 \pagestyle{headings}
 \sloppy
 
 \parindent 0pt\parskip 0.5ex
 
 \isabellestyle{literalunderscore}
 
 \railtermfont{\isabellestyle{tt}}
 \railnontermfont{\isabellestyle{literalunderscore}}
 \railnamefont{\isabellestyle{literalunderscore}}