--- a/src/Cube/ROOT.ML Mon Oct 20 10:53:42 1997 +0200
+++ b/src/Cube/ROOT.ML Mon Oct 20 11:01:07 1997 +0200
@@ -9,6 +9,8 @@
val banner = "Barendregt's Lambda-Cube";
writeln banner;
+reset global_names;
+
print_depth 1;
use_thy "Cube";
--- a/src/LCF/ROOT.ML Mon Oct 20 10:53:42 1997 +0200
+++ b/src/LCF/ROOT.ML Mon Oct 20 11:01:07 1997 +0200
@@ -11,6 +11,8 @@
val banner = "Logic for Computable Functions (in FOL)";
writeln banner;
+reset global_names;
+
print_depth 1;
use_thy "LCF";
use"simpdata.ML";