src/HOL/ex/ROOT.ML

--- a/src/HOL/ex/ROOT.ML	Fri Jan 25 14:53:55 2008 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Jan 25 14:53:56 2008 +0100
@@ -9,12 +9,17 @@
   "GCD",
   "Eval",
   "State_Monad",
-  "Code_Integer",
-  "Efficient_Nat",
+  "Efficient_Nat_examples",
+  "ExecutableContent",
+  "FuncSet",
+  "Word",
+  "Eval_Examples",
+  "Random"
+];
+
+no_document use_thys [
   "Codegenerator",
-  "Codegenerator_Pretty",
-  "FuncSet",
-  "Word"
+  "Codegenerator_Pretty"
 ];
 
 use_thys [
@@ -49,8 +54,6 @@
   "Unification",
   "Commutative_RingEx",
   "Commutative_Ring_Complete",
-  "Eval_Examples",
-  "Random",
   "Primrec",
   "Tarski",
   "Adder",