src/HOLCF/FOCUS/ROOT.ML

--- a/src/HOLCF/FOCUS/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
+++ b/src/HOLCF/FOCUS/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
@@ -6,9 +6,4 @@
 See README.html for further information.
 *)
 
-val banner = "HOLCF/FOCUS";
-writeln banner;
-
-with_path "~~/src/HOLCF/ex" use_thy "Fstreams";
-use_thy "FOCUS";
-use_thy "Buffer_adm";
+use_thys ["Fstreams", "FOCUS", "Buffer_adm"];