# 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";