hide internal structures (again);
authorwenzelm
Mon, 23 Jul 2007 14:06:14 +0200
changeset 23923 8c10f3515633
parent 23922 707639e9497d
child 23924 883359757a56
hide internal structures (again);
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;