# HG changeset patch
# User wenzelm
# Date 1201298727 -3600
# Node ID bcb1e9b7644b05040f4edbd728e982e343e9cc61
# Parent  0cb35fa9c6fa8d56b34ca1da19d186355d9d0209
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
more simultaneous use_thys;

diff -r 0cb35fa9c6fa -r bcb1e9b7644b src/HOL/ex/ROOT.ML
--- 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"];
+