src/Pure/Syntax/syntax.ML
changeset 23923 8c10f3515633
parent 23660 18765718cf62
child 24247 9d0bb01f6634
equal deleted inserted replaced
23922:707639e9497d 23923:8c10f3515633
   560 
   560 
   561 end;
   561 end;
   562 
   562 
   563 structure BasicSyntax: BASIC_SYNTAX = Syntax;
   563 structure BasicSyntax: BASIC_SYNTAX = Syntax;
   564 open BasicSyntax;
   564 open BasicSyntax;
       
   565 
       
   566 structure Hidden = struct end;
       
   567 structure Lexicon = Hidden;
       
   568 structure Ast = Hidden;
       
   569 structure SynExt = Hidden;
       
   570 structure Parser = Hidden;
       
   571 structure TypeExt = Hidden;
       
   572 structure SynTrans = Hidden;
       
   573 structure Mixfix = Hidden;
       
   574 structure Printer = Hidden;