src/Pure/Syntax/syntax.ML
changeset 42284 326f57825e1a
parent 42280 e7f3652c280c
child 42287 d98eb048a2e4
--- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 13:31:16 2011 +0200
@@ -7,7 +7,6 @@
 
 signature BASIC_SYNTAX =
 sig
-  include SYN_TRANS0
   include MIXFIX0
   include PRINTER0
 end;
@@ -16,7 +15,6 @@
 sig
   include LEXICON0
   include SYN_EXT0
-  include SYN_TRANS1
   include MIXFIX1
   include PRINTER0
   val positions_raw: Config.raw
@@ -727,7 +725,7 @@
 
 (*export parts of internal Syntax structures*)
 val syntax_tokenize = tokenize;
-open Lexicon Syn_Ext Syn_Trans Mixfix Printer;
+open Lexicon Syn_Ext Mixfix Printer;
 val tokenize = syntax_tokenize;
 
 end;