diff -r fad9b7479dbe -r 74c01296e818 src/CCL/IsaMakefile
--- a/src/CCL/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
+++ b/src/CCL/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
@@ -4,33 +4,46 @@
 # IsaMakefile for CCL
 #
 
+## targets
+
+default: CCL
+images: CCL
+test: CCL-ex
+all: images test
+
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \
-	    Gfp.thy Gfp.ML Lfp.thy Lfp.ML
+
+## CCL
+
+CCL: FOL $(OUT)/CCL
 
-CCL_FILES = CCL.thy CCL.ML Term.thy Term.ML Type.thy Type.ML \
-	    coinduction.ML Hered.thy Hered.ML Trancl.thy Trancl.ML \
-	    Wfd.thy Wfd.ML genrec.ML typecheck.ML eval.ML Fix.thy Fix.ML
+FOL:
+	@cd $(SRC)/FOL; $(ISATOOL) make FOL
 
-EX_FILES = ex/ROOT.ML ex/Flag.ML ex/Flag.thy ex/List.ML ex/List.thy \
-	   ex/Nat.ML ex/Nat.thy ex/Stream.ML ex/Stream.thy
-
-
-$(OUT)/CCL: $(OUT)/FOL $(SET_FILES) $(CCL_FILES)
+$(OUT)/CCL: $(OUT)/FOL CCL.ML CCL.thy Fix.ML Fix.thy Gfp.ML Gfp.thy \
+  Hered.ML Hered.thy Lfp.ML Lfp.thy ROOT.ML Set.ML Set.thy Term.ML \
+  Term.thy Trancl.ML Trancl.thy Type.ML Type.thy Wfd.ML Wfd.thy \
+  coinduction.ML equalities.ML eval.ML genrec.ML mono.ML subset.ML \
+  typecheck.ML
 	@$(ISATOOL) usedir -b $(OUT)/FOL CCL
 
-$(OUT)/FOL:
-	@cd ../FOL; $(ISATOOL) make
+
+## CCL-ex
 
-$(LOG)/CCL-ex.gz: ex/ROOT.ML $(OUT)/CCL $(EX_FILES)
+CCL-ex: CCL $(LOG)/CCL-ex.gz
+
+$(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.ML ex/Flag.thy ex/List.ML \
+  ex/List.thy ex/Nat.ML ex/Nat.thy ex/ROOT.ML ex/Stream.ML ex/Stream.thy
 	@$(ISATOOL) usedir $(OUT)/CCL ex
 
-test: $(OUT)/CCL $(LOG)/CCL-ex.gz
+
+## clean
 
 clean:
-	@rm -f $(OUT)/CCL $(LOG)/CCL-ex.gz
-
-
-.PRECIOUS: $(OUT)/FOL $(OUT)/CCL
+	@rm -f $(OUT)/CCL $(LOG)/CCL.gz $(LOG)/CCL-ex.gz