src/HOL/IsaMakefile
changeset 28312 f0838044f034
parent 28243 84d90ec67059
child 28327 4d7a0a941b79
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 22 08:00:28 2008 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 22 13:55:59 2008 +0200
     1.3 @@ -71,8 +71,7 @@
     1.4  
     1.5  $(OUT)/Pure: Pure
     1.6  
     1.7 -$(OUT)/HOL-Plain: $(OUT)/Pure \
     1.8 -  plain.ML \
     1.9 +PLAIN_DEPENDENCIES = $(OUT)/Pure \
    1.10    Code_Setup.thy \
    1.11    Datatype.thy \
    1.12    Divides.thy \
    1.13 @@ -178,10 +177,11 @@
    1.14    $(SRC)/Tools/nbe.ML \
    1.15    $(SRC)/Tools/random_word.ML \
    1.16    $(SRC)/Tools/rat.ML
    1.17 +
    1.18 +$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
    1.19  	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
    1.20  
    1.21 -$(OUT)/HOL: $(OUT)/HOL-Plain \
    1.22 -  ROOT.ML \
    1.23 +$(OUT)/HOL: ROOT.ML $(PLAIN_DEPENDENCIES) \
    1.24    Arith_Tools.thy \
    1.25    ATP_Linkup.thy \
    1.26    Code_Eval.thy \
    1.27 @@ -278,7 +278,7 @@
    1.28    Tools/TFL/usyntax.ML \
    1.29    Tools/TFL/utils.ML \
    1.30    Tools/watcher.ML
    1.31 -	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/HOL-Plain HOL
    1.32 +	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
    1.33  
    1.34  
    1.35  ## HOL-Library