src/Pure/Isar/ROOT.ML
changeset 24219 e558fe311376
parent 23896 26f92c405337
child 24306 7798a0f37253
--- a/src/Pure/Isar/ROOT.ML	Fri Aug 10 17:04:24 2007 +0200
+++ b/src/Pure/Isar/ROOT.ML	Fri Aug 10 17:04:34 2007 +0200
@@ -43,10 +43,9 @@
 use "net_rules.ML";
 use "induct_attrib.ML";
 
-(*code generator base*)
-use "../Tools/codegen_consts.ML";
-use "../Tools/codegen_func.ML";
-use "../Tools/codegen_data.ML";
+(*executable theory content*)
+use "code_unit.ML";
+use "code.ML";
 
 (*derived theory and proof elements*)
 use "local_theory.ML";
@@ -54,7 +53,7 @@
 use "obtain.ML";
 use "locale.ML";
 use "spec_parse.ML";
-use "../Tools/class_package.ML";
+use "class.ML";
 use "theory_target.ML";
 use "specification.ML";
 use "constdefs.ML";