# HG changeset patch
# User clasohm
# Date 751293315 -3600
# Node ID 099d949fe46778aaf8d4747786cfd64393a0a644
# Parent  729fe026c5f35576e5cb75a2f036d4cc438c10cd
changes for new Readthy

diff -r 729fe026c5f3 -r 099d949fe467 src/CCL/ROOT.ML
--- a/src/CCL/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
+++ b/src/CCL/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
@@ -11,7 +11,7 @@
 (* Higher-Order Set Theory Extension to FOL *)
 (*      used as basis for CCL               *)
 
-(*set_load_path [".", "../FOL"]; wait for new Readthy*)
+set_loadpath [".", "../FOL"];
 
 use_thy "set";
 use     "subset.ML";
diff -r 729fe026c5f3 -r 099d949fe467 src/CTT/ROOT.ML
--- a/src/CTT/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
+++ b/src/CTT/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
@@ -12,6 +12,9 @@
 
 print_depth 1;  
 
+structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+open Readthy;
+
 use_thy"ctt";
 use "../Provers/typedsimp.ML";
 use "rew.ML";
diff -r 729fe026c5f3 -r 099d949fe467 src/Cube/ROOT.ML
--- a/src/Cube/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
+++ b/src/Cube/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
@@ -9,6 +9,9 @@
 val banner = "Barendregt's Lambda-Cube";
 writeln banner;
 
+structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+open Readthy;
+
 print_depth 1;  
 use_thy "cube";
 
diff -r 729fe026c5f3 -r 099d949fe467 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
+++ b/src/FOL/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
@@ -11,6 +11,9 @@
 
 writeln banner;
 
+structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+open Readthy;
+
 print_depth 1;  
 use_thy "ifol";
 use_thy "fol";
diff -r 729fe026c5f3 -r 099d949fe467 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
+++ b/src/FOLP/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
@@ -12,6 +12,9 @@
 
 writeln banner;
 
+structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+open Readthy;
+
 print_depth 1;  
 use_thy "ifolp";
 use_thy "folp";
diff -r 729fe026c5f3 -r 099d949fe467 src/LCF/ROOT.ML
--- a/src/LCF/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
+++ b/src/LCF/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
@@ -11,6 +11,8 @@
 val banner = "Logic for Computable Functions (in FOL)";
 writeln banner;
 
+set_loadpath [".", "../FOL"];
+
 print_depth 1;
 use_thy "lcf";
 use"simpdata.ML";
diff -r 729fe026c5f3 -r 099d949fe467 src/LK/ROOT.ML
--- a/src/LK/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
+++ b/src/LK/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
@@ -10,6 +10,9 @@
 val banner = "Classical First-Order Sequent Calculus";
 writeln banner;
 
+structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+open Readthy;
+
 print_depth 1;  
 
 use_thy "lk";
diff -r 729fe026c5f3 -r 099d949fe467 src/Modal/ROOT.ML
--- a/src/Modal/ROOT.ML	Fri Oct 22 11:42:02 1993 +0100
+++ b/src/Modal/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
@@ -7,6 +7,8 @@
 val banner = "Modal Logic (over LK)";
 writeln banner;
 
+set_loadpath [".", "../LK"];
+
 use_thy "modal0";
 
 structure Modal0_rls =