src/FOLP/ROOT.ML

 
 val banner = "First-Order Logic with Natural Deduction with Proof Terms";
 
 writeln banner;
 
-structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
-open Readthy;
+init_thy_reader();
 
 print_depth 1;  
 use_thy "IFOLP";
 use_thy "FOLP";