# HG changeset patch
# User wenzelm
# Date 877963396 -3600
# Node ID 59cac65fb751590ce9f41e36378ccdfd496ef57e
# Parent  6d9bec7b0b9e2bf216b48d7c746f1f5f0b04e256
do not change global_names flag;

diff -r 6d9bec7b0b9e -r 59cac65fb751 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Mon Oct 27 15:29:01 1997 +0100
+++ b/src/HOLCF/ROOT.ML	Mon Oct 27 15:43:16 1997 +0100
@@ -10,8 +10,6 @@
 val banner = "HOLCF";
 writeln banner;
 
-set global_names;
-
 print_depth 1;
 
 use_thy "HOLCF";