--- a/src/Pure/Syntax/README Mon May 18 18:08:58 1998 +0200
+++ b/src/Pure/Syntax/README Mon May 18 18:10:04 1998 +0200
@@ -8,7 +8,8 @@
Pretty (generic pretty printing module)
Scan (generic scanner toolbox)
- Symbol (baroque characters)
+ Source (co-algebraic data sources)
+ Symbol (generalized characters)
Syntax (internal interface to the syntax module)
BasicSyntax (part of Syntax made pervasive)
--- a/src/Pure/Syntax/ROOT.ML Mon May 18 18:08:58 1998 +0200
+++ b/src/Pure/Syntax/ROOT.ML Mon May 18 18:10:04 1998 +0200
@@ -5,9 +5,13 @@
This file builds the syntax module.
*)
+(*generic modules*)
use "pretty.ML";
use "scan.ML";
+use "source.ML";
use "symbol.ML";
+
+(*actual syntax module*)
use "lexicon.ML";
use "token_trans.ML";
use "ast.ML";