different session branches for HOL-Plain vs. Plain
--- 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