# HG changeset patch
# User wenzelm
# Date 848334545 -3600
# Node ID 0dddd9575717d10bf44d06d2cf3ca8000096c8cc
# Parent  e895937fcd56d53778d2e79b7ec79e431f255b74
added symbol_font.ML;

diff -r e895937fcd56 -r 0dddd9575717 src/Pure/Syntax/ROOT.ML
--- a/src/Pure/Syntax/ROOT.ML	Mon Nov 18 17:28:40 1996 +0100
+++ b/src/Pure/Syntax/ROOT.ML	Mon Nov 18 17:29:05 1996 +0100
@@ -5,6 +5,7 @@
 This file builds the syntax module.
 *)
 
+use "symbol_font.ML";
 use "pretty.ML";
 use "lexicon.ML";
 use "ast.ML";