src/Pure/Syntax/syntax.ML
changeset 15833 78109c7012ed
parent 15759 144c9f9a8ade
child 16613 76e57e08dcb5
--- a/src/Pure/Syntax/syntax.ML	Sat Apr 23 19:51:11 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Apr 23 19:51:24 2005 +0200
@@ -15,7 +15,6 @@
 
 signature SYNTAX =
 sig
-  include TOKEN_TRANS0
   include AST1
   include LEXICON0
   include SYN_EXT0
@@ -500,9 +499,8 @@
 
 
 
-(** export parts of internal Syntax structures **)
-
-open TokenTrans Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
+(*export parts of internal Syntax structures*)
+open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
 
 end;