# HG changeset patch
# User wenzelm
# Date 857144209 -3600
# Node ID d696d7e17046b80a11c79e8eec62347d443992e1
# Parent  dabe8ab631fadf9e90296fcd43f61ae9daf8ec60
added token_trans.ML;

diff -r dabe8ab631fa -r d696d7e17046 src/Pure/Syntax/ROOT.ML
--- a/src/Pure/Syntax/ROOT.ML	Fri Feb 28 15:52:16 1997 +0100
+++ b/src/Pure/Syntax/ROOT.ML	Fri Feb 28 16:36:49 1997 +0100
@@ -9,6 +9,7 @@
 use "lexicon.ML";
 structure Scanner: SCANNER = Lexicon;
 use "symbol_font.ML";
+use "token_trans.ML";
 use "ast.ML";
 use "syn_ext.ML";
 use "parser.ML";