src/Pure/Syntax/syntax.ML
changeset 15833 78109c7012ed
parent 15759 144c9f9a8ade
child 16613 76e57e08dcb5
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Apr 23 19:51:11 2005 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Apr 23 19:51:24 2005 +0200
     1.3 @@ -15,7 +15,6 @@
     1.4  
     1.5  signature SYNTAX =
     1.6  sig
     1.7 -  include TOKEN_TRANS0
     1.8    include AST1
     1.9    include LEXICON0
    1.10    include SYN_EXT0
    1.11 @@ -500,9 +499,8 @@
    1.12  
    1.13  
    1.14  
    1.15 -(** export parts of internal Syntax structures **)
    1.16 -
    1.17 -open TokenTrans Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    1.18 +(*export parts of internal Syntax structures*)
    1.19 +open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    1.20  
    1.21  end;
    1.22