# HG changeset patch
# User wenzelm
# Date 1160177468 -7200
# Node ID b853d43268945133d6e688cf4b1d07ca2112d8d1
# Parent  ac46f01024be8651d8e18e981baf4d531c5bdf80
added Isar/theory_target.ML;

diff -r ac46f01024be -r b853d4326894 src/Pure/IsaMakefile
--- 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		\
diff -r ac46f01024be -r b853d4326894 src/Pure/Isar/ROOT.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";