diff -r da00b32c3977 -r 7972e16d2dd3 ROOT.ML
--- a/ROOT.ML	Sun Oct 17 17:33:40 1993 +0100
+++ b/ROOT.ML	Fri Oct 22 13:36:28 1993 +0100
@@ -10,6 +10,9 @@
 val banner = "Higher-Order Logic";
 writeln banner;
 
+structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+open Readthy;
+
 print_depth 1;  
 eta_contract := true;
 use_thy "hol";