diff -r 5eb3020f7a03 -r 7892b76adb5b src/Pure/Makefile
--- a/src/Pure/Makefile	Tue Jan 11 08:10:18 1994 +0100
+++ b/src/Pure/Makefile	Tue Jan 11 11:36:32 1994 +0100
@@ -25,7 +25,7 @@
 	drule.ML tctical.ML tactic.ML goals.ML install_pp.ML
 
 SYNTAX_FILES =  Syntax/ROOT.ML	Syntax/ast.ML		Syntax/xgram.ML\
-	Syntax/extension.ML	Syntax/lexicon.ML	Syntax/parse_tree.ML\
+	Syntax/extension.ML	Syntax/lexicon.ML\
 	Syntax/parser.ML	Syntax/type_ext.ML	Syntax/sextension.ML\
 	Syntax/pretty.ML	Syntax/printer.ML	Syntax/syntax.ML\
 	Syntax/earley0A.ML