diff -r e43d91f31118 -r 71e33d95ac55 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Thu Dec 20 13:58:45 2007 +0100
+++ b/src/Pure/General/ROOT.ML	Thu Dec 20 14:33:40 2007 +0100
@@ -16,7 +16,6 @@
 use "../ML/ml_parse.ML";
 use "secure.ML";
 
-use "random_word.ML";
 use "integer.ML";
 use "stack.ML";
 use "heap.ML";