--- a/src/FOL/ROOT.ML Tue Oct 28 17:37:46 1997 +0100 +++ b/src/FOL/ROOT.ML Tue Oct 28 17:41:15 1997 +0100 @@ -11,8 +11,6 @@ writeln banner; -reset global_names; - print_depth 1; use "../Provers/simplifier.ML";