diff -r d00238af17b6 -r 5f33ce0ed21f lib/Tools/mkdir
--- a/lib/Tools/mkdir	Thu Jul 30 23:50:11 2009 +0200
+++ b/lib/Tools/mkdir	Fri Jul 31 11:34:14 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