author | wenzelm |
Mon, 23 Jul 2007 14:06:14 +0200 | |
changeset 23923 | 8c10f3515633 |
parent 23922 | 707639e9497d |
child 23924 | 883359757a56 |
--- 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;