--- a/src/Cube/ROOT.ML Tue Oct 28 17:37:46 1997 +0100 +++ b/src/Cube/ROOT.ML Tue Oct 28 17:41:15 1997 +0100 @@ -9,8 +9,6 @@ val banner = "Barendregt's Lambda-Cube"; writeln banner; -reset global_names; - print_depth 1; use_thy "Cube";