diff -r 8aeb7ec8003a -r a4c985fe015d src/Tools/WWW_Find/ROOT.ML
--- a/src/Tools/WWW_Find/ROOT.ML	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/ROOT.ML	Mon May 30 17:07:48 2011 +0200
@@ -10,5 +10,6 @@
   use "scgi_req.ML";
   use "scgi_server.ML";
   use "echo.ML";
+  use "html_templates.ML";
   use "find_theorems.ML")
 else ()