# HG changeset patch
# User wenzelm
# Date 1003766541 -7200
# Node ID d9509f71498294fe23b36abbd6a31cca5bfeab4d
# Parent  7099c865de3b7dbfff53eec5f1408cd01d19b883
rearrange sources for locales;

diff -r 7099c865de3b -r d9509f714982 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Mon Oct 22 18:02:04 2001 +0200
+++ b/src/Pure/Isar/ROOT.ML	Mon Oct 22 18:02:21 2001 +0200
@@ -7,9 +7,11 @@
 *)
 
 (*basic proof engine*)
+use "object_logic.ML";
 use "auto_bind.ML";
 use "rule_cases.ML";
 use "proof_context.ML";
+use "locale.ML";
 use "proof.ML";
 use "proof_data.ML";
 use "proof_history.ML";
@@ -20,8 +22,8 @@
 use "method.ML";
 
 (*derived proof elements*)
-use "local_defs.ML";
 use "calculation.ML";
+use "obtain.ML";
 use "skip_proof.ML";
 
 (*outer syntax*)
@@ -45,20 +47,21 @@
 use "isar_syn.ML";
 
 (*main ML interfaces*)
-use "obtain.ML";
 use "isar.ML";
 
 structure PureIsar =
 struct
+  structure ObjectLogic = ObjectLogic;
   structure AutoBind = AutoBind;
   structure ProofContext = ProofContext;
+  structure Locale = Locale;
   structure Proof = Proof;
   structure ProofHistory = ProofHistory;
   structure Args = Args;
   structure Attrib = Attrib;
   structure Method = Method;
-  structure LocalDefs = LocalDefs;
   structure Calculation = Calculation;
+  structure Obtain = Obtain;
   structure SkipProof = SkipProof;
   structure OuterLex = OuterLex;
   structure Antiquote = Antiquote;
@@ -72,6 +75,5 @@
   structure ThyHeader = ThyHeader;
   structure OuterSyntax = OuterSyntax;
   structure IsarSyn = IsarSyn;
-  structure Obtain = Obtain;
   structure Isar = Isar;
 end;