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;