src/Pure/Syntax/syntax.ML
changeset 23923 8c10f3515633
parent 23660 18765718cf62
child 24247 9d0bb01f6634
--- 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;