--- a/src/Pure/Tools/ROOT.ML Thu May 31 20:55:32 2007 +0200
+++ b/src/Pure/Tools/ROOT.ML Thu May 31 20:55:33 2007 +0200
@@ -9,7 +9,6 @@
(*derived theory and proof elements*)
use "invoke.ML";
-(* use "class_package.ML"; see Pure/Isar/ROOT.ML *)
(*code generator, 1st generation*)
use "../codegen.ML";
@@ -21,12 +20,6 @@
use "codegen_serializer.ML";
use "codegen_package.ML";
-(*Steven Obua's evaluator*)
-use "am_interpreter.ML";
-use "am_compiler.ML";
-use "am_util.ML";
-use "compute.ML";
-
(*norm-by-eval*)
use "nbe_eval.ML";
use "nbe_codegen.ML";