# HG changeset patch
# User wenzelm
# Date 877338067 -7200
# Node ID ea440c63d206eb29f4ae997183940cadaff75d48
# Parent  1d5bee4d047f3832ec50228ca5c6e6cd5686ff9a
qualified names;

diff -r 1d5bee4d047f -r ea440c63d206 src/Cube/ROOT.ML
--- 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";
diff -r 1d5bee4d047f -r ea440c63d206 src/LCF/ROOT.ML
--- 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";