1.1 --- a/src/CCL/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
     1.2 +++ b/src/CCL/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  (* Higher-Order Set Theory Extension to FOL *)
     1.5  (*      used as basis for CCL               *)
     1.6  
     1.7 -(*set_load_path [".", "../FOL"]; wait for new Readthy*)
     1.8 +set_loadpath [".", "../FOL"];
     1.9  
    1.10  use_thy "set";
    1.11  use     "subset.ML";

     2.1 --- a/src/CTT/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
     2.2 +++ b/src/CTT/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
     2.3 @@ -12,6 +12,9 @@
     2.4  
     2.5  print_depth 1;  
     2.6  
     2.7 +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
     2.8 +open Readthy;
     2.9 +
    2.10  use_thy"ctt";
    2.11  use "../Provers/typedsimp.ML";
    2.12  use "rew.ML";

     3.1 --- a/src/Cube/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
     3.2 +++ b/src/Cube/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
     3.3 @@ -9,6 +9,9 @@
     3.4  val banner = "Barendregt's Lambda-Cube";
     3.5  writeln banner;
     3.6  
     3.7 +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
     3.8 +open Readthy;
     3.9 +
    3.10  print_depth 1;  
    3.11  use_thy "cube";
    3.12  

     4.1 --- a/src/FOL/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
     4.2 +++ b/src/FOL/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
     4.3 @@ -11,6 +11,9 @@
     4.4  
     4.5  writeln banner;
     4.6  
     4.7 +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
     4.8 +open Readthy;
     4.9 +
    4.10  print_depth 1;  
    4.11  use_thy "ifol";
    4.12  use_thy "fol";

     5.1 --- a/src/FOLP/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
     5.2 +++ b/src/FOLP/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
     5.3 @@ -12,6 +12,9 @@
     5.4  
     5.5  writeln banner;
     5.6  
     5.7 +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
     5.8 +open Readthy;
     5.9 +
    5.10  print_depth 1;  
    5.11  use_thy "ifolp";
    5.12  use_thy "folp";

     6.1 --- a/src/LCF/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
     6.2 +++ b/src/LCF/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
     6.3 @@ -11,6 +11,8 @@
     6.4  val banner = "Logic for Computable Functions (in FOL)";
     6.5  writeln banner;
     6.6  
     6.7 +set_loadpath [".", "../FOL"];
     6.8 +
     6.9  print_depth 1;
    6.10  use_thy "lcf";
    6.11  use"simpdata.ML";

     7.1 --- a/src/LK/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
     7.2 +++ b/src/LK/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
     7.3 @@ -10,6 +10,9 @@
     7.4  val banner = "Classical First-Order Sequent Calculus";
     7.5  writeln banner;
     7.6  
     7.7 +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
     7.8 +open Readthy;
     7.9 +
    7.10  print_depth 1;  
    7.11  
    7.12  use_thy "lk";

     8.1 --- a/src/Modal/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
     8.2 +++ b/src/Modal/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
     8.3 @@ -7,6 +7,8 @@
     8.4  val banner = "Modal Logic (over LK)";
     8.5  writeln banner;
     8.6  
     8.7 +set_loadpath [".", "../LK"];
     8.8 +
     8.9  use_thy "modal0";
    8.10  
    8.11  structure Modal0_rls =