# HG changeset patch
# User haftmann
# Date 1222084559 -7200
# Node ID f0838044f034379aeeaf860ba0bb6067f759d2af
# Parent  b86feb50ca58d17d8171218cf109cde7737ae898
different session branches for HOL-Plain vs. Plain

diff -r b86feb50ca58 -r f0838044f034 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