diff -r 729fe026c5f3 -r 099d949fe467 src/LK/ROOT.ML --- a/src/LK/ROOT.ML Fri Oct 22 11:42:02 1993 +0100 +++ b/src/LK/ROOT.ML Fri Oct 22 13:35:15 1993 +0100 @@ -10,6 +10,9 @@ val banner = "Classical First-Order Sequent Calculus"; writeln banner; +structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); +open Readthy; + print_depth 1; use_thy "lk";