diff -r 6967a42a8496 -r e2af92a3281b doc-src/System/system.tex
--- a/doc-src/System/system.tex	Mon Sep 22 17:37:24 1997 +0200
+++ b/doc-src/System/system.tex	Mon Sep 22 17:37:48 1997 +0200
@@ -14,11 +14,10 @@
 \author{{\em Lawrence C. Paulson}\\
         Computer Laboratory \\ University of Cambridge \\
         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
-        With Contributions by Tobias Nipkow and Markus Wenzel}
-%FIXME not yet
-%        \thanks{Section~\protect\ref{sec:html} was written by Carsten
-%          Clasohm.  Chapter~\protect\ref{sec:browse} was written by Stefan
-%          Berghofer. Other parts are by Markus Wenzel.}
+        With Contributions by Tobias Nipkow and Markus Wenzel
+        \thanks{Section~\protect\ref{sec:html} was written by Carsten
+          Clasohm.  Chapter~\protect\ref{sec:browse} was written by Stefan
+          Berghofer. Other parts are by Markus Wenzel.}}
 
 \makeindex