src/LK/ROOT.ML

 *)
 
 val banner = "Classical First-Order Sequent Calculus";
 writeln banner;
 
-structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
-open Readthy;
+init_thy_reader();
 
 print_depth 1;  
 
 use_thy "LK";