# HG changeset patch
# User wenzelm
# Date 758986115 -3600
# Node ID a8ff0932d78a53ded3162523cbd30a0690b1e1c7
# Parent  8b2a8c52242d96759faff816d3154ba1e43f26b1
changed SYNTAX_FILES;

diff -r 8b2a8c52242d -r a8ff0932d78a src/Pure/Makefile
--- a/src/Pure/Makefile	Wed Jan 19 14:27:46 1994 +0100
+++ b/src/Pure/Makefile	Wed Jan 19 14:28:35 1994 +0100
@@ -24,11 +24,10 @@
 	sequence.ML envir.ML pattern.ML unify.ML logic.ML thm.ML net.ML\
 	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_FILES =  Syntax/ROOT.ML	Syntax/ast.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
+	Syntax/earley0A.ML	Syntax/syn_ext.ML
 
 THY_FILES = Thy/ROOT.ML Thy/scan.ML Thy/parse.ML Thy/syntax.ML Thy/read.ML