diff -r af069653f1d7 -r a04bf731ceb6 doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Mon Sep 04 19:49:39 2006 +0200
+++ b/doc-src/IsarImplementation/implementation.tex	Mon Sep 04 20:07:55 2006 +0200
@@ -18,7 +18,9 @@
   \\[4ex] The Isabelle/Isar Implementation}
 \author{\emph{Makarius Wenzel}}
 
-\makeglossary
+%FIXME
+%\makeglossary
+
 \makeindex
 
 
@@ -78,8 +80,9 @@
 \bibliography{../manual}
 \endgroup
 
-\tocentry{\glossaryname}
-\printglossary
+%FIXME
+%\tocentry{\glossaryname}
+%\printglossary
 
 \tocentry{\indexname}
 \printindex