src/HOL/ROOT.ML

--- a/src/HOL/ROOT.ML	Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/ROOT.ML	Mon Oct 20 11:25:39 1997 +0200
@@ -7,9 +7,11 @@
 Should be executed in the subdirectory HOL.
 *)
 
-val banner = "Higher-Order Logic with curried functions";
+val banner = "Higher-Order Logic";
 writeln banner;
 
+reset global_names;
+
 print_depth 1;
 
 (* Add user sections *)