diff -r e2b06bfe471a -r 5cbe966d67a2 src/Pure/Tools/ROOT.ML
--- a/src/Pure/Tools/ROOT.ML	Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Tools/ROOT.ML	Fri Apr 20 11:21:42 2007 +0200
@@ -15,9 +15,6 @@
 use "../codegen.ML";
 
 (*code generator, 2nd generation*)
-use "codegen_consts.ML";
-use "codegen_func.ML";
-use "codegen_data.ML";
 use "codegen_names.ML";
 use "codegen_funcgr.ML";
 use "codegen_thingol.ML";