# HG changeset patch # User wenzelm # Date 1165510721 -3600 # Node ID 6947e32b61717093dc8843399e53eb34754e7b9b # Parent 826ab43d43f5a6cb9c69a6747f705bb5982f6f88 added Isar/term_syntax.ML; diff -r 826ab43d43f5 -r 6947e32b6171 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Dec 07 17:58:39 2006 +0100 +++ b/src/Pure/IsaMakefile Thu Dec 07 17:58:41 2006 +0100 @@ -41,8 +41,8 @@ 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/theory_target.ML Isar/thy_header.ML \ - Isar/toplevel.ML ML-Systems/polyml-4.1.4-patch.ML \ + Isar/term_style.ML Isar/term_syntax.ML Isar/theory_target.ML \ + Isar/thy_header.ML Isar/toplevel.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-5.0.ML ML-Systems/polyml-interrupt-timeout.ML \ ML-Systems/polyml-posix.ML ML-Systems/polyml.ML ML-Systems/poplogml.ML \ diff -r 826ab43d43f5 -r 6947e32b6171 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Thu Dec 07 17:58:39 2006 +0100 +++ b/src/Pure/Isar/ROOT.ML Thu Dec 07 17:58:41 2006 +0100 @@ -34,6 +34,7 @@ (*derived theory and proof elements*) use "local_theory.ML"; +use "term_syntax.ML"; use "calculation.ML"; use "obtain.ML"; use "locale.ML";