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";