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