# HG changeset patch
# User wenzelm
# Date 857144335 -3600
# Node ID 484ec6ca0c506b1413e637c832fb72d8d46265b3
# Parent  d696d7e17046b80a11c79e8eec62347d443992e1
added Syntax/token_trans.ML;

diff -r d696d7e17046 -r 484ec6ca0c50 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Feb 28 16:36:49 1997 +0100
+++ b/src/Pure/IsaMakefile	Fri Feb 28 16:38:55 1997 +0100
@@ -19,9 +19,9 @@
 	Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML \
 	Syntax/parser.ML Syntax/pretty.ML Syntax/printer.ML \
 	Syntax/symbol_font.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
-	Syntax/syntax.ML Syntax/type_ext.ML Thy/ROOT.ML Thy/symbol_input.ML \
-	Thy/thm_database.ML Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML \
-	Thy/thy_syn.ML axclass.ML basis.ML deriv.ML display.ML drule.ML \
+	Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML\
+	Thy/symbol_input.ML Thy/thm_database.ML Thy/thy_parse.ML Thy/thy_read.ML \
+	Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML deriv.ML display.ML drule.ML \
 	envir.ML goals.ML install_pp.ML library.ML logic.ML net.ML pattern.ML \
 	search.ML section_utils.ML sequence.ML sign.ML symtab.ML tactic.ML \
 	tctical.ML term.ML theory.ML thm.ML type.ML unify.ML \
diff -r d696d7e17046 -r 484ec6ca0c50 src/Pure/Makefile
--- 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