--- a/src/HOL/ex/ROOT.ML Sat Sep 17 18:11:25 2005 +0200
+++ b/src/HOL/ex/ROOT.ML Sat Sep 17 18:11:26 2005 +0200
@@ -51,4 +51,4 @@
no_document use_thy "Word";
time_use_thy "Adder";
-no_document time_use_thy "Hebrew";
+HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";