diff -r 30d874dc7000 -r 3951ced4156c src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 17:18:38 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 17:55:50 2014 +0100
@@ -42,6 +42,8 @@
 
 \urlstyle{tt}
 
+\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
+
 \begin{document}
 
 %%% TYPESETTING