--- a/src/CTT/ROOT.ML Tue Jul 28 17:03:12 1998 +0200 +++ b/src/CTT/ROOT.ML Tue Jul 28 17:05:34 1998 +0200 @@ -10,8 +10,6 @@ val banner = "Constructive Type Theory"; writeln banner; -reset global_names; - print_depth 1; use_thy "CTT";