do not change global_names flag;
authorwenzelm
Mon, 27 Oct 1997 15:43:16 +0100
changeset 4010 59cac65fb751
parent 4009 6d9bec7b0b9e
child 4011 c161162bc8c5
do not change global_names flag;
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";