Added dependence on Thy/thm_database.ML
authornipkow
Thu Jun 01 12:31:52 1995 +0200 (1995-06-01)
changeset 11400a804a71274a
parent 1139 993e475e70e2
child 1141 a94c0ab9a3ed
Added dependence on Thy/thm_database.ML
src/Pure/Makefile
     1.1 --- a/src/Pure/Makefile	Wed May 31 10:46:46 1995 +0200
     1.2 +++ b/src/Pure/Makefile	Thu Jun 01 12:31:52 1995 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  	Syntax/syn_ext.ML	Syntax/mixfix.ML
     1.5  
     1.6  THY_FILES = Thy/ROOT.ML		Thy/thy_scan.ML		Thy/thy_parse.ML\
     1.7 -	Thy/thy_syn.ML		Thy/thy_read.ML
     1.8 +	Thy/thy_syn.ML		Thy/thy_read.ML		Thy/thm_database.ML
     1.9  
    1.10  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    1.11  $(BIN)/Pure:   $(FILES)  $(SYNTAX_FILES)  $(THY_FILES)  $(ML_DBASE)