--- a/src/Doc/Datatypes/Datatypes.thy Fri Apr 17 17:19:41 2020 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Apr 17 17:32:11 2020 +0200
@@ -124,8 +124,8 @@
to register arbitrary type constructors as BNFs.
\item Section
-\ref{sec:deriving-destructors-and-theorems-for-free-constructors},
-``Deriving Destructors and Theorems for Free Constructors,'' explains how to
+\ref{sec:deriving-destructors-and-constructor-theorems},
+``Deriving Destructors and Constructor Theorems,'' explains how to
use the command @{command free_constructors} to derive destructor constants
and theorems for freely generated types, as performed internally by
@{command datatype} and @{command codatatype}.
@@ -3229,8 +3229,8 @@
\<close>
-section \<open>Deriving Destructors and Theorems for Free Constructors
- \label{sec:deriving-destructors-and-theorems-for-free-constructors}\<close>
+section \<open>Deriving Destructors and Constructor Theorems
+ \label{sec:deriving-destructors-and-constructor-theorems}\<close>
text \<open>
The derivation of convenience theorems for types equipped with free constructors,
--- a/src/Doc/Datatypes/document/root.tex Fri Apr 17 17:19:41 2020 +0200
+++ b/src/Doc/Datatypes/document/root.tex Fri Apr 17 17:32:11 2020 +0200
@@ -17,13 +17,6 @@
\usepackage{pdfsetup}
\usepackage{railsetup}
\usepackage{framed}
-\usepackage{xpatch}
-
-\makeatletter
-\xpatchcmd{\chaptermark}{\MakeUppercase}{}{}{}%
-\xpatchcmd{\sectionmark}{\MakeUppercase}{}{}{}%
-\xpatchcmd*{\tableofcontents}{\MakeUppercase}{}{}{}%
-\makeatother
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{3}