# HG changeset patch
# User wenzelm
# Date 850218666 -3600
# Node ID 74c99949ad84c898f7e8b0924b3093db20aac8fc
# Parent  1b6bc618c35600d13fb41e6bb1e86032f9747cca
*** empty log message ***

diff -r 1b6bc618c356 -r 74c99949ad84 src/Pure/Syntax/ROOT.ML
--- a/src/Pure/Syntax/ROOT.ML	Tue Dec 10 12:50:35 1996 +0100
+++ b/src/Pure/Syntax/ROOT.ML	Tue Dec 10 12:51:06 1996 +0100
@@ -5,9 +5,10 @@
 This file builds the syntax module.
 *)
 
-use "symbol_font.ML";
 use "pretty.ML";
 use "lexicon.ML";
+structure Scanner: SCANNER = Lexicon;
+use "symbol_font.ML";
 use "ast.ML";
 use "syn_ext.ML";
 use "parser.ML";
@@ -17,8 +18,6 @@
 use "printer.ML";
 use "syntax.ML";
 
-(*Hiding: only the most basic features are opened*)
+(*hiding: only the most basic features are opened*)
 structure BasicSyntax: BASIC_SYNTAX = Syntax;
 open BasicSyntax;
-
-structure Scanner: SCANNER = Lexicon;