# HG changeset patch
# User wenzelm
# Date 1114278615 -7200
# Node ID 5fdf2d8dab9c71532e3e30af349b79667e2c52dd
# Parent  e9b4c9feb296141fbd19b39a87c043fd59c87dfb
removed isar.ML;
removed structure PureIsar;

diff -r e9b4c9feb296 -r 5fdf2d8dab9c src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Sat Apr 23 19:50:05 2005 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sat Apr 23 19:50:15 2005 +0200
@@ -27,7 +27,6 @@
 use "skip_proof.ML";
 
 (*outer syntax*)
-(*use "outer_lex.ML";*)   (*see ../Thy/ROOT.ML*)
 use "antiquote.ML";
 use "outer_parse.ML";
 
@@ -45,40 +44,3 @@
 use "constdefs.ML";
 use "isar_cmd.ML";
 use "isar_syn.ML";
-
-(*main ML interfaces*)
-use "isar.ML";
-
-structure PureIsar =
-struct
-  structure ObjectLogic = ObjectLogic;
-  structure AutoBind = AutoBind;
-  structure RuleCases = RuleCases;
-  structure ProofContext = ProofContext;
-  structure ContextRules = ContextRules;
-  structure Args = Args;
-  structure Attrib = Attrib;
-  structure Locale = Locale;
-  structure Proof = Proof;
-  structure ProofHistory = ProofHistory;
-  structure NetRules = NetRules;
-  structure InductAttrib = InductAttrib;
-  structure Method = Method;
-  structure Calculation = Calculation;
-  structure Obtain = Obtain;
-  structure SkipProof = SkipProof;
-  structure OuterLex = OuterLex;
-  structure Antiquote = Antiquote;
-  structure OuterParse = OuterParse;
-  structure Toplevel = Toplevel;
-  structure Session = Session;
-  structure IsarOutput = IsarOutput;
-  structure ThyHeader = ThyHeader;
-  structure OuterSyntax = OuterSyntax;
-  structure IsarThy = IsarThy;
-  structure Constdefs = Constdefs;
-  structure IsarCmd = IsarCmd;
-  structure IsarSyn = IsarSyn;
-  structure Isar = Isar;
-end;
-