doc-src/IsarImplementation/Thy/document/ML.tex

--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Sep 12 17:45:58 2006 +0200
@@ -35,7 +35,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME beyond the basis library definition%
+FIXME beyond the NJ basis library proposal%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %