src/FOL/ROOT.ML

 
 val banner = "First-Order Logic with Natural Deduction";
 
 writeln banner;
 
-structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
-open Readthy;
+init_thy_reader();
 
 print_depth 1;  
 use_thy "FOL";
 
 use "../Provers/hypsubst.ML";