# HG changeset patch
# User wenzelm
# Date 1249032854 -7200
# Node ID 5f33ce0ed21f3402b2c29668c87bae74dc6f0328
# Parent  d00238af17b69db99ac88c109afefa25e960512d
modernized generated example session;

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