src/Pure/ROOT.ML
changeset 36959 f5417836dbea
parent 36955 226fb165833e
child 36961 7b14afc02fc4
--- a/src/Pure/ROOT.ML	Mon May 17 15:05:32 2010 +0200
+++ b/src/Pure/ROOT.ML	Mon May 17 15:11:25 2010 +0200
@@ -167,7 +167,7 @@
 use "Proof/proofchecker.ML";
 
 (*outer syntax*)
-use "Isar/outer_lex.ML";
+use "Isar/token.ML";
 use "Isar/keyword.ML";
 use "Isar/parse.ML";
 use "Isar/parse_value.ML";
@@ -299,6 +299,13 @@
 struct
 
 structure OuterKeyword = Keyword;
+
+structure OuterLex =
+struct
+  open Token;
+  type token = T;
+end;
+
 structure OuterParse = Parse;
 structure OuterSyntax = Outer_Syntax;
 structure SpecParse = Parse_Spec;