diff -r ce2b8e6502f9 -r 7a3b5bbed313 doc-src/IsarImplementation/implementation.tex
--- a/doc-src/IsarImplementation/implementation.tex	Mon Feb 16 21:04:15 2009 +0100
+++ b/doc-src/IsarImplementation/implementation.tex	Mon Feb 16 21:23:33 2009 +0100
@@ -20,9 +20,6 @@
   and Larry Paulson
 }
 
-%FIXME
-%\makeglossary
-
 \makeindex
 
 
@@ -85,10 +82,6 @@
 \bibliography{../manual}
 \endgroup
 
-%FIXME
-%\tocentry{\glossaryname}
-%\printglossary
-
 \tocentry{\indexname}
 \printindex