--- a/doc-src/IsarRef/isar-ref.tex	Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Mon May 08 11:13:28 2000 +0200
@@ -120,6 +120,6 @@
   \bibliography{../manual}
 \endgroup
 
-\input{isar-ref.ind}
+\printindex
 
 \end{document}
changeset 8828	5be2d1745c61
parent 8596	b2ef22670f25
child 8896	c80aba8c1d5e