# 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;