diff -r a9dc0484c903 -r 3c056eab237c src/LCF/ROOT.ML --- a/src/LCF/ROOT.ML Tue Oct 28 17:37:46 1997 +0100 +++ b/src/LCF/ROOT.ML Tue Oct 28 17:41:15 1997 +0100 @@ -11,8 +11,6 @@ val banner = "Logic for Computable Functions (in FOL)"; writeln banner; -reset global_names; - print_depth 1; use_thy "LCF"; use"simpdata.ML";