set global_names;
authorwenzelm
Mon Oct 20 12:47:44 1997 +0200 (1997-10-20)
changeset 3953473ea5ce5ca8
parent 3952 dca1bce88ec8
child 3954 c8c188655948
set global_names;
src/HOLCF/ROOT.ML
     1.1 --- a/src/HOLCF/ROOT.ML	Mon Oct 20 12:47:02 1997 +0200
     1.2 +++ b/src/HOLCF/ROOT.ML	Mon Oct 20 12:47:44 1997 +0200
     1.3 @@ -10,6 +10,8 @@
     1.4  val banner = "HOLCF";
     1.5  writeln banner;
     1.6  
     1.7 +set global_names;
     1.8 +
     1.9  print_depth 1;
    1.10  
    1.11  use_thy "HOLCF";