diff -r b8703f63bfb2 -r 3f697c636fa1 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Dec 03 20:38:58 2010 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Dec 03 21:30:41 2010 +0100
@@ -8,7 +8,10 @@
   "Efficient_Nat_examples",
   "FuncSet",
   "Eval_Examples",
-  "Normalization_by_Evaluation"
+  "Normalization_by_Evaluation",
+  "Hebrew",
+  "Chinese",
+  "Serbian"
 ];
 
 use_thys [
@@ -71,9 +74,6 @@
   "Birthday_Paradoxon"
 ];
 
-HTML.with_charset "utf-8" (no_document use_thys)
-  ["Hebrew", "Chinese", "Serbian"];
-
 use_thy "SVC_Oracle";
 if getenv "SVC_HOME" = "" then ()
 else use_thy "svc_test";