# HG changeset patch
# User wenzelm
# Date 889456222 -3600
# Node ID ff89fc67cc7a66c8e1b24dde9c5777583cc58990
# Parent  6aa25ee18fc41e35193907a83379c77186863812
scan.ML, symbol.ML;

diff -r 6aa25ee18fc4 -r ff89fc67cc7a src/Pure/Syntax/ROOT.ML
--- 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";