src/Pure/Syntax/ROOT.ML
changeset 4940 dd4bbbcd1d22
parent 4696 ff89fc67cc7a
child 5230 fdc28193ccf7
--- 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";