diff -r 7c01dc2dcb8c -r 869e485bbdba src/Doc/Ref/document/root.tex
--- a/src/Doc/Ref/document/root.tex	Sun Nov 04 19:51:53 2012 +0100
+++ b/src/Doc/Ref/document/root.tex	Sun Nov 04 20:01:26 2012 +0100
@@ -1,10 +1,6 @@
 \documentclass[12pt,a4paper]{report}
 \usepackage{graphicx,iman,extra,ttbox,proof,pdfsetup}
 
-%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
-%%% to delete old ones:  \\indexbold{\*[^}]*}
-%% run    sedindex ref    to prepare index file
-%%% needs chapter on Provers/typedsimp.ML?
 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Isabelle Reference Manual}
 
 \author{{\em Lawrence C. Paulson}\\
@@ -12,8 +8,6 @@
         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
         With Contributions by Tobias Nipkow and Markus Wenzel}  
 
-\makeindex
-
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
 
 \pagestyle{headings}
@@ -61,5 +55,4 @@
   \bibliography{manual}
 \endgroup
 
-\printindex
 \end{document}