diff --git a/src/Doc/Datatypes/document/root.tex b/src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex
+++ b/src/Doc/Datatypes/document/root.tex
@@ -1,93 +1,93 @@
 \documentclass[12pt,a4paper]{article} % fleqn
 \usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{amsfonts}
 \usepackage{amsmath}
 \usepackage{cite}
 \usepackage{enumitem}
 \usepackage{footmisc}
 \usepackage{latexsym}
 \usepackage{graphicx}
 \usepackage{iman}
 \usepackage{extra}
 \usepackage{isar}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{style}
 \usepackage{pdfsetup}
 \usepackage{railsetup}
 \usepackage{framed}
-\usepackage{regexpatch}
+\usepackage{xpatch}
 
 \makeatletter
 \xpatchcmd{\chaptermark}{\MakeUppercase}{}{}{}%
 \xpatchcmd{\sectionmark}{\MakeUppercase}{}{}{}%
 \xpatchcmd*{\tableofcontents}{\MakeUppercase}{}{}{}%
 \makeatother
 
 \setcounter{secnumdepth}{3}
 \setcounter{tocdepth}{3}
 
 \renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
 
 \newbox\boxA
 \setbox\boxA=\hbox{\ }
 \parindent=4\wd\boxA
 
 \newcommand\blankline{\vskip-.25\baselineskip}
 
 \newenvironment{indentblock}{\list{}{\setlength{\leftmargin}{\parindent}}\item[]}{\endlist}
 
 \newcommand{\keyw}[1]{\textbf{#1}}
 \newcommand{\synt}[1]{\textit{#1}}
 \newcommand{\hthm}[1]{\textbf{\textit{#1}}}
 
 %\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$}
 \renewcommand\isactrlsub[1]{\/$\sb{#1}$}
 \renewcommand\isadigit[1]{\/\ensuremath{\mathrm{#1}}}
 \renewcommand\isacharprime{\isamath{{'}\mskip-2mu}}
 \renewcommand\isacharunderscore{\mbox{\_}}
 \renewcommand\isacharunderscorekeyword{\mbox{\_}}
 \renewcommand\isachardoublequote{\mbox{\upshape{``}}}
 \renewcommand\isachardoublequoteopen{\mbox{\upshape{``}\kern.1ex}}
 \renewcommand\isachardoublequoteclose{\/\kern.15ex\mbox{\upshape{''}}}
 \renewcommand{\isasyminverse}{\isamath{{}^{-}}}
 
 \hyphenation{isa-belle}
 
 \isadroptag{theory}
 
 \title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
 Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL}
 \author{Julian Biendarra, Jasmin Blanchette, \\
 Martin Desharnais, Lorenz Panny, \\
 Andrei Popescu, and Dmitriy Traytel}
 
 \urlstyle{tt}
 
 \begin{document}
 
 \maketitle
 
 \begin{sloppy}
 \begin{abstract}
 \noindent
 This tutorial describes the definitional package for datatypes and codatatypes,
 and for primitively recursive and corecursive functions, in Isabelle/HOL. The
 following commands are provided:
 \keyw{datatype}, \keyw{datatype_\allowbreak compat}, \keyw{prim\-rec}, \keyw{co\-data\-type},
 \keyw{prim\-co\-rec}, \keyw{prim\-co\-recursive}, \keyw{bnf}, \keyw{lift_\allowbreak bnf},
 \keyw{copy_\allowbreak bnf}, \keyw{bnf_\allowbreak axiom\-atization},
 \keyw{print_\allowbreak bnfs}, and \keyw{free_\allowbreak constructors}.
 \end{abstract}
 \end{sloppy}
 
 \tableofcontents
 
 \input{Datatypes.tex}
 
 \let\em=\sl
 \bibliography{manual}{}
 \bibliographystyle{abbrv}
 
 \end{document}