author | wenzelm |
Mon, 09 Mar 1998 16:10:22 +0100 | |
changeset 4696 | ff89fc67cc7a |
parent 4695 | 6aa25ee18fc4 |
child 4697 | 101d384b69b2 |
--- a/src/Pure/Syntax/ROOT.ML Mon Mar 09 16:09:56 1998 +0100 +++ b/src/Pure/Syntax/ROOT.ML Mon Mar 09 16:10:22 1998 +0100 @@ -6,9 +6,9 @@ *) use "pretty.ML"; +use "scan.ML"; +use "symbol.ML"; use "lexicon.ML"; -structure Scanner: SCANNER = Lexicon; -use "symbol_font.ML"; use "token_trans.ML"; use "ast.ML"; use "syn_ext.ML";