# HG changeset patch
# User clasohm
# Date 751293825 -3600
# Node ID 144ec40f2650d3d507a19714be6219a366a44ecc
# Parent  208ab8773a7320926803bd36bc2476355f74955a
added -h 15000 for Poly/ML in Makefile,
changed ROOT.ML for new Readthy

diff -r 208ab8773a73 -r 144ec40f2650 src/ZF/Makefile
--- a/src/ZF/Makefile	Fri Oct 22 13:42:51 1993 +0100
+++ b/src/ZF/Makefile	Fri Oct 22 13:43:45 1993 +0100
@@ -32,7 +32,7 @@
 $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
 	case "$(COMP)" in \
 	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
-		echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\
+		echo 'open PolyML; use"ROOT";' | $(COMP) -h 15000 $(BIN)/ZF ;;\
 	sml*)	echo 'use"ROOT.ML"; xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;;\
 	*)	echo Bad value for ISABELLECOMP;;\
 	esac
@@ -42,7 +42,7 @@
 
 test:   ex/ROOT.ML  $(BIN)/ZF
 	case "$(COMP)" in \
-	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\
+	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) -h 15000 $(BIN)/ZF ;;\
 	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\
 	*)	echo Bad value for ISABELLECOMP;;\
 	esac
diff -r 208ab8773a73 -r 144ec40f2650 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Fri Oct 22 13:42:51 1993 +0100
+++ b/src/ZF/ROOT.ML	Fri Oct 22 13:43:45 1993 +0100
@@ -11,6 +11,8 @@
 val banner = "ZF Set Theory (in FOL)";
 writeln banner;
 
+set_loadpath [".", "ex", "../FOL"];
+
 (*For Pure/tactic??  A crude way of adding structure to rules*)
 fun CHECK_SOLVED (Tactic tf) = 
   Tactic (fn state => 
@@ -66,7 +68,7 @@
 use     "datatype.ML";
 
 use     "fin.ML";
-use     "list.ML";
+use_thy "List";
 use_thy "listfn";
 
 (*printing functions are inherited from FOL*)