--- a/src/Pure/IsaMakefile Sat Oct 07 01:31:07 2006 +0200
+++ b/src/Pure/IsaMakefile Sat Oct 07 01:31:08 2006 +0200
@@ -41,7 +41,7 @@
Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML \
Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML \
Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML Isar/specification.ML \
- Isar/term_style.ML Isar/thy_header.ML Isar/toplevel.ML \
+ Isar/term_style.ML Isar/theory_target.ML Isar/thy_header.ML Isar/toplevel.ML \
ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML \
ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML \
ML-Systems/polyml-4.9.1.ML ML-Systems/polyml-interrupt-timeout.ML \
--- a/src/Pure/Isar/ROOT.ML Sat Oct 07 01:31:07 2006 +0200
+++ b/src/Pure/Isar/ROOT.ML Sat Oct 07 01:31:08 2006 +0200
@@ -33,11 +33,12 @@
use "induct_attrib.ML";
(*derived theory and proof elements*)
+use "local_theory.ML";
use "calculation.ML";
use "obtain.ML";
use "locale.ML";
use "../axclass.ML";
-use "local_theory.ML";
+use "theory_target.ML";
use "specification.ML";
use "constdefs.ML";