Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
more simultaneous use_thys;

--- a/src/HOL/ex/ROOT.ML	Fri Jan 25 23:05:25 2008 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Jan 25 23:05:27 2008 +0100
@@ -17,10 +17,8 @@
   "Random"
 ];
 
-no_document use_thys [
-  "Codegenerator",
-  "Codegenerator_Pretty"
-];
+no_document use_thy "Codegenerator";
+no_document use_thy "Codegenerator_Pretty";
 
 use_thys [
   "Higher_Order_Logic",
@@ -89,5 +87,5 @@
 time_use_thy "Quickcheck_Examples";
 no_document time_use_thy "NormalForm";
 
-HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
-HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";
+HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"];
+