# HG changeset patch
# User wenzelm
# Date 1185192374 -7200
# Node ID 8c10f3515633a6874213884299bc63afd1b83ca3
# Parent  707639e9497d96c15208935915a8249eefc5bae5
hide internal structures (again);

diff -r 707639e9497d -r 8c10f3515633 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Jul 23 14:06:12 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Jul 23 14:06:14 2007 +0200
@@ -562,3 +562,13 @@
 
 structure BasicSyntax: BASIC_SYNTAX = Syntax;
 open BasicSyntax;
+
+structure Hidden = struct end;
+structure Lexicon = Hidden;
+structure Ast = Hidden;
+structure SynExt = Hidden;
+structure Parser = Hidden;
+structure TypeExt = Hidden;
+structure SynTrans = Hidden;
+structure Mixfix = Hidden;
+structure Printer = Hidden;