eliminated Pure/Isar/comment.ML;
authorwenzelm
Tue, 12 Feb 2002 20:35:35 +0100
changeset 12882e20f14f7ff35
parent 12881 eeb36b66480e
child 12883 3f86b73d592d
eliminated Pure/Isar/comment.ML;
src/Pure/Isar/ROOT.ML
     1.1 --- a/src/Pure/Isar/ROOT.ML	Tue Feb 12 20:34:02 2002 +0100
     1.2 +++ b/src/Pure/Isar/ROOT.ML	Tue Feb 12 20:35:35 2002 +0100
     1.3 @@ -30,7 +30,6 @@
     1.4  (*outer syntax*)
     1.5  (*use "outer_lex.ML";*)   (*see ../Thy/ROOT.ML*)
     1.6  use "antiquote.ML";
     1.7 -use "comment.ML";
     1.8  use "outer_parse.ML";
     1.9  
    1.10  (*toplevel environment*)
    1.11 @@ -67,7 +66,6 @@
    1.12    structure SkipProof = SkipProof;
    1.13    structure OuterLex = OuterLex;
    1.14    structure Antiquote = Antiquote;
    1.15 -  structure Comment = Comment;
    1.16    structure OuterParse = OuterParse;
    1.17    structure Toplevel = Toplevel;
    1.18    structure Session = Session;