different session branches for HOL-Plain vs. Plain
authorhaftmann
Mon, 22 Sep 2008 13:55:59 +0200
changeset 28312 f0838044f034
parent 28311 b86feb50ca58
child 28313 1742947952f8
different session branches for HOL-Plain vs. Plain
src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Sep 22 08:00:28 2008 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 22 13:55:59 2008 +0200
@@ -71,8 +71,7 @@
 
 $(OUT)/Pure: Pure
 
-$(OUT)/HOL-Plain: $(OUT)/Pure \
-  plain.ML \
+PLAIN_DEPENDENCIES = $(OUT)/Pure \
   Code_Setup.thy \
   Datatype.thy \
   Divides.thy \
@@ -178,10 +177,11 @@
   $(SRC)/Tools/nbe.ML \
   $(SRC)/Tools/random_word.ML \
   $(SRC)/Tools/rat.ML
+
+$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
 	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
 
-$(OUT)/HOL: $(OUT)/HOL-Plain \
-  ROOT.ML \
+$(OUT)/HOL: ROOT.ML $(PLAIN_DEPENDENCIES) \
   Arith_Tools.thy \
   ATP_Linkup.thy \
   Code_Eval.thy \
@@ -278,7 +278,7 @@
   Tools/TFL/usyntax.ML \
   Tools/TFL/utils.ML \
   Tools/watcher.ML
-	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/HOL-Plain HOL
+	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
 
 
 ## HOL-Library