merged

--- a/lib/Tools/mkdir	Sat Aug 01 00:17:03 2009 +0200
+++ b/lib/Tools/mkdir	Sat Aug 01 00:39:45 2009 +0200
@@ -187,8 +187,8 @@
   [ -z "$QUIET" ] && echo "creating $PREFIX/ROOT.ML" >&2
   cat >ROOT.ML <<EOF
 (*
-  no_document use_thy "ThisTheory";
-  use_thy "ThatTheory";
+  no_document use_thys ["This_Theory1", "This_Theory2"];
+  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
 *)
 EOF
 fi