# HG changeset patch
# User nipkow
# Date 802002712 -7200
# Node ID 0a804a71274aa9689c147bf1dbec2e1d50819216
# Parent  993e475e70e249fd7f54394c883850e14c71e3ec
Added dependence on Thy/thm_database.ML

diff -r 993e475e70e2 -r 0a804a71274a src/Pure/Makefile
--- a/src/Pure/Makefile	Wed May 31 10:46:46 1995 +0200
+++ b/src/Pure/Makefile	Thu Jun 01 12:31:52 1995 +0200
@@ -31,7 +31,7 @@
 	Syntax/syn_ext.ML	Syntax/mixfix.ML
 
 THY_FILES = Thy/ROOT.ML		Thy/thy_scan.ML		Thy/thy_parse.ML\
-	Thy/thy_syn.ML		Thy/thy_read.ML
+	Thy/thy_syn.ML		Thy/thy_read.ML		Thy/thm_database.ML
 
 #Uses cp rather than make_database because Poly/ML allows only 3 levels
 $(BIN)/Pure:   $(FILES)  $(SYNTAX_FILES)  $(THY_FILES)  $(ML_DBASE)