# HG changeset patch
# User blanchet
# Date 1587137531 -7200
# Node ID 3b36fc4916afb9741cccf308c89fa49669d5f4e8
# Parent  c7d19729456c6d3b1963379225c1f0ed8db51f3e
removed LaTeX package and hack to avoid ALLCAPS headers

diff -r c7d19729456c -r 3b36fc4916af src/Doc/Datatypes/Datatypes.thy
--- 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,
diff -r c7d19729456c -r 3b36fc4916af src/Doc/Datatypes/document/root.tex
--- 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}