diff -r aaeee16a56f5 -r ec0fbd1a852b src/HOL/Isar_Examples/document/root.tex
--- a/src/HOL/Isar_Examples/document/root.tex	Sun Feb 14 16:39:43 2016 +0100
+++ b/src/HOL/Isar_Examples/document/root.tex	Sun Feb 14 16:40:00 2016 +0100
@@ -5,10 +5,6 @@
 \isabellestyle{it}
 \usepackage{pdfsetup}\urlstyle{rm}
 
-\renewcommand{\isacommand}[1]
-{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
-  {\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}
-
 \newcommand{\DUMMYPROOF}{{\langle\mathit{proof}\rangle}}
 \newcommand{\dummyproof}{$\DUMMYPROOF$}