--- a/src/CCL/Makefile Fri Oct 15 12:51:21 1993 +0100
+++ b/src/CCL/Makefile Sun Oct 17 16:30:16 1993 +0100
@@ -22,9 +22,9 @@
SET_FILES = ROOT.ML set.thy set.ML subset.ML equalities.ML mono.ML \
gfp.thy gfp.ML lfp.thy lfp.ML
-CCL_FILES = ccl.thy ccl.ML terms.thy terms.ML types.thy types.ML \
+CCL_FILES = ccl.thy ccl.ML term.thy term.ML type.thy type.ML \
coinduction.ML hered.thy hered.ML trancl.thy trancl.ML\
- wf.thy wf.ML genrec.ML typecheck.ML eval.ML fix.thy fix.ML
+ wfd.thy wfd.ML genrec.ML typecheck.ML eval.ML fix.thy fix.ML
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/CCL: $(BIN)/FOL $(SET_FILES) $(CCL_FILES)
--- a/src/CCL/ROOT.ML Fri Oct 15 12:51:21 1993 +0100
+++ b/src/CCL/ROOT.ML Sun Oct 17 16:30:16 1993 +0100
@@ -11,6 +11,8 @@
(* Higher-Order Set Theory Extension to FOL *)
(* used as basis for CCL *)
+(*set_load_path [".", "../FOL"]; wait for new Readthy*)
+
use_thy "set";
use "subset.ML";
use "equalities.ML";
@@ -22,13 +24,13 @@
(* with evaluation to weak head-normal form *)
use_thy "ccl";
-use_thy "terms";
-use_thy "types";
+use_thy "term";
+use_thy "type";
use "coinduction.ML";
use_thy "hered";
use_thy "trancl";
-use_thy "wf";
+use_thy "wfd";
use "genrec.ML";
use "typecheck.ML";
use "eval.ML";