src/Pure/Tools/ROOT.ML
changeset 20939 a81ce849e9f4
parent 20708 29c1754b250f
child 22023 487b79b95a20
--- a/src/Pure/Tools/ROOT.ML	Tue Oct 10 09:17:24 2006 +0200
+++ b/src/Pure/Tools/ROOT.ML	Tue Oct 10 09:18:09 2006 +0200
@@ -14,7 +14,6 @@
 
 (*code generator, 2nd generation*)
 use "codegen_consts.ML";
-use "codegen_simtype.ML";
 use "codegen_data.ML";
 use "codegen_names.ML";
 use "codegen_funcgr.ML";