src/Pure/Makefile
changeset 2692 484ec6ca0c50
parent 2235 866dbb04816c
child 2960 a6b56d03ed0d
--- a/src/Pure/Makefile	Fri Feb 28 16:36:49 1997 +0100
+++ b/src/Pure/Makefile	Fri Feb 28 16:38:55 1997 +0100
@@ -31,7 +31,8 @@
 SYNTAX_FILES =	Syntax/ROOT.ML	Syntax/ast.ML		Syntax/lexicon.ML\
 	Syntax/parser.ML	Syntax/type_ext.ML	Syntax/syn_trans.ML\
 	Syntax/pretty.ML	Syntax/printer.ML	Syntax/syntax.ML\
-	Syntax/syn_ext.ML	Syntax/mixfix.ML	Syntax/symbol_font.ML
+	Syntax/syn_ext.ML	Syntax/mixfix.ML	Syntax/symbol_font.ML\
+	Syntax/token_trans.ML
 
 THY_FILES = Thy/ROOT.ML		Thy/thy_scan.ML		Thy/thy_parse.ML\
 	Thy/thy_syn.ML		Thy/thy_read.ML		Thy/thm_database.ML