src/LK/ROOT.ML

 *)
 
 val banner = "Classical First-Order Sequent Calculus";
 writeln banner;
 
+structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+open Readthy;
+
 print_depth 1;  
 
 use_thy "lk";
 
 use "../Pure/install_pp.ML";