diff -r 25d9d836ed9c -r 326f57825e1a src/Pure/Syntax/syntax.ML --- 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;