src/HOL/ex/ROOT.ML

--- a/src/HOL/ex/ROOT.ML	Tue Mar 27 09:19:37 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Mar 27 12:28:42 2007 +0200
@@ -9,7 +9,7 @@
 
 no_document time_use_thy "Classpackage";
 no_document time_use_thy "Eval_examples";
-no_document time_use_thy "CodeRandom";
+no_document time_use_thy "Random";
 no_document time_use_thy "Codegenerator_Rat";
 no_document time_use_thy "Codegenerator";