Added dependence on Thy/thm_database.ML
authornipkow
Thu, 01 Jun 1995 12:31:52 +0200
changeset 1140 0a804a71274a
parent 1139 993e475e70e2
child 1141 a94c0ab9a3ed
Added dependence on Thy/thm_database.ML
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)