author | wenzelm |
Tue, 05 Apr 2011 14:30:40 +0200 | |
changeset 42225 | cf48af306290 |
parent 42224 | 578a51fae383 |
child 42226 | cb650789f2f0 |
--- a/src/Pure/Syntax/syntax.ML Tue Apr 05 14:25:18 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue Apr 05 14:30:40 2011 +0200 @@ -941,7 +941,7 @@ (*export parts of internal Syntax structures*) -open Lexicon Syn_Ext Parser Type_Ext Syn_Trans Mixfix Printer; +open Lexicon Syn_Ext Type_Ext Syn_Trans Mixfix Printer; end; @@ -949,7 +949,6 @@ open Basic_Syntax; forget_structure "Syn_Ext"; -forget_structure "Parser"; forget_structure "Type_Ext"; forget_structure "Syn_Trans"; forget_structure "Mixfix";