# HG changeset patch
# User wenzelm
# Date 1302006640 -7200
# Node ID cf48af3062900ca3ee7abd43390c43ed7f4291e7
# Parent  578a51fae383be3f86cea0d6d29e09a01af28604
discontinued special treatment of structure Parser -- directly accessible;

diff -r 578a51fae383 -r cf48af306290 src/Pure/Syntax/syntax.ML
--- 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";