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*)