# HG changeset patch
# User haftmann
# Date 1228156946 -3600
# Node ID 043a42ba2a4db73a21e6b77747fbb6fd92801c20
# Parent  128459bd72d22f3356e360f6301eb49069ec25db# Parent  32542abe665656daaf3018350e12efa9a629cdf3
merged

diff -r 128459bd72d2 -r 043a42ba2a4d .hgtags
--- a/.hgtags	Mon Dec 01 19:41:16 2008 +0100
+++ b/.hgtags	Mon Dec 01 19:42:26 2008 +0100
@@ -1,39 +1,25 @@
 0140ff702b232f48cb4c7414dca663e41acad213 Isabelle94-3
 0a604b2fc2b1df524a3cf81f5a7b2255b19fda92 Isabelle99
 0b268cff9344268b18ab5241b5c45e3374f107cd Isabelle94-8
-18cfe8facb793bc11b17771ac1ef6c93dd5a94c1 lsf_1999_12_22
 213dcc39358faefae737f8e7d2eea67658e9eedf Isabelle2003
 23ceb1dc9755a8ad6f0230697d0cc52f54102bf4 Isabelle94-5
 2cf13a72e1704d0094d21e7dc68e7271a282ed31 Isabelle2008
 33b9b5da3e6faee6ca6969d17e79634d49e5b46a Isabelle94-1
-33e290a704457e9f33cec1a8beec48b40b8b1430 vc_branch_point
 35fba71ec6ef550178e5f5e44d95d96c6f36eae6 nominal_01
 3e47692e3a3e4c695f6345b3534ed0c36817fd40 Isabelle99-2
 50be659d4222b68f95e9c966097e59091f26acf3 Isabelle99-1
-5156b731ebc81578a4e63ec3999020eaab6dbeb6 isa2005_RC3
-644dddf4e932a2a80d22cd8d1abbb7fec88b7232 haftmann_at_in_tum_de_20050622
-659b8165c7248e1ef46ed7700b983fc81764d02f ballarin_2006_branch_point
 67692db44c7099ad8789f088003213aeb095e914 Isabelle94-2
 6a422b22ba02f6275fa3ac5f9df1428705552d50 Isabelle98-1
-6f0928a942d152c71fd2cafad4302cfd82f3a25c vc_last_merge
 6f79698f294df13edfba9c790df18a545570c81e Isabelle2007
 7d6b0241afabbf87d4d94a412a1c1ebbba71c088 Isabelle94-4
 805fa01ac2337790fd555991f1231d3ef6b2e3fb Isabelle2004_0
 831a9a7ab9f352c65b0f449630b428304c89362b Isabelle93
 836950047d8508e3c200edc1e07a46c2c5e09cd7 Isabelle94-6
-849ec3962b55c97454a20ae95e8cd8c2e8c3be15 haftmann_at_in_tum_de_20050629
 8d42a7bccf0b0880dff8e46c71c4811be8b2e7ec Isabelle94-7
-9dab1e491d105fe99a94ab89c5d1b5ad561b467c isa2005_RC4
-9dac2cad550097d381c7572ae69fcb0c9a3d7edc preBCV
 a23af144eb47f12354dff090813c796f278e2eb8 nominal_03
-a59af3a83c613f5a535988b8a6b535ca37054776 vc_merge
 be6b5edbca9ffeb3bace5f4bac5c6478bf8cbdb2 Isabelle98
-cbfd12c61a1fc6e284a218b58259d3c2909ba4cd isa2005_RC1
 cd41a57221d07441647284e239b8d8d77d498ef5 isa94
 ce180e5b7fa056003791fff19cc5cefba193b135 Isabelle2002
 dde117622dace696123b023d1f06cf8d8ef9eb46 nominal_02
-e50f95ccde996846d01183b18419c9b86ca96c0b haftmann_at_in_tum_de_2005_08_28
-f1275d2a1deed16b48a51e298f4a895747c949af working-10-06-2005
-f3cafd2929d5b9b4d3690536021c97418865c423 wide_types_start
 f9eb0f819642b2ad77119dbf8935bf13248f205d Isabelle94
 fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
diff -r 128459bd72d2 -r 043a42ba2a4d Admin/Mercurial/convert
--- a/Admin/Mercurial/convert	Mon Dec 01 19:41:16 2008 +0100
+++ b/Admin/Mercurial/convert	Mon Dec 01 19:42:26 2008 +0100
@@ -19,9 +19,9 @@
 export HGRCPATH="$THIS/cvs/Admin/Mercurial/hgrc"
 
 cd "$THIS"
-/home/isabelle/mercurial/bin/hg convert --filemap cvs/Admin/Mercurial/filemap cvs hg >> "$LOG" 2>&1 || exit 2
+/home/isabelle/mercurial/bin/hg convert --filemap cvs/Admin/Mercurial/filemap cvs isabelle-cvs >> "$LOG" 2>&1 || exit 2
 
-[ -e hg/.hg/hgrc ] || ln -s ../../cvs/Admin/Mercurial/hgrc hg/.hg/hgrc
+[ -e isabelle-cvs/.hg/hgrc ] || ln -s ../../cvs/Admin/Mercurial/hgrc isabelle-cvs/.hg/hgrc
 
 
 ## logrotate
diff -r 128459bd72d2 -r 043a42ba2a4d Admin/Mercurial/hgrc
--- a/Admin/Mercurial/hgrc	Mon Dec 01 19:41:16 2008 +0100
+++ b/Admin/Mercurial/hgrc	Mon Dec 01 19:42:26 2008 +0100
@@ -6,6 +6,6 @@
 
 [web]
 style = isabelle
-description = Snapshot of the official Isabelle CVS repository
+description = Snapshot of the old Isabelle CVS
 allow_archive = gz
 maxfiles = 50
diff -r 128459bd72d2 -r 043a42ba2a4d Admin/Mercurial/hgwebdir.cgi
--- a/Admin/Mercurial/hgwebdir.cgi	Mon Dec 01 19:41:16 2008 +0100
+++ b/Admin/Mercurial/hgwebdir.cgi	Mon Dec 01 19:42:26 2008 +0100
@@ -4,7 +4,7 @@
 
 # adjust python path if not a system-wide install:
 import sys
-sys.path.insert(0, "/home/isabelle-repository/repos/mercurial-www4/lib64/python2.4/site-packages")
+sys.path.insert(0, "/home/isabelle-repository/repos/mercurial-www4/lib64/python2.5/site-packages")
 
 # enable importing on demand to reduce startup time
 from mercurial import demandimport; demandimport.enable()
diff -r 128459bd72d2 -r 043a42ba2a4d Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Mon Dec 01 19:41:16 2008 +0100
+++ b/Admin/isatest/isatest-makedist	Mon Dec 01 19:42:26 2008 +0100
@@ -11,7 +11,7 @@
 TMP=/tmp/isatest-makedist.$$
 MAIL=$HOME/bin/pmail
 
-MAKEDIST=$HOME/bin/makedist_mercurial
+MAKEDIST=$HOME/bin/makedist
 MAKEALL=$HOME/bin/isatest-makeall
 TAR=tar
 CVS2CL="$HOME/bin/cvs2cl --follow-only TRUNK"
diff -r 128459bd72d2 -r 043a42ba2a4d Admin/makedist
--- a/Admin/makedist	Mon Dec 01 19:41:16 2008 +0100
+++ b/Admin/makedist	Mon Dec 01 19:42:26 2008 +0100
@@ -2,18 +2,13 @@
 #
 # $Id$
 #
-# makedist -- make Isabelle source distribution.
-
+# makedist -- make Isabelle source distribution
 
 ## global settings
 
-DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
-SRCS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents Tools ZF"
+REPOS="http://isabelle.in.tum.de/repos/isabelle"
 
-export CVSROOT=/home/isabelle-repository/archive
-[ ! -d "$CVSROOT" ] && CVSROOT="${ISABELLE_USER:-$USER}@atbroy100.informatik.tu-muenchen.de:$CVSROOT"
-
-[ -z "$CVS2CL" ] && type -path cvs2cl >/dev/null && CVS2CL=cvs2cl
+DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
 
 umask 022
 
@@ -27,16 +22,15 @@
 {
   cat <<EOF
 
-Usage: $PRG VERSION [NAME]
+Usage: $PRG [OPTIONS] [VERSION]
 
-  Make Isabelle distribution from the master sources at TUM.
+  Options are:
+    -r RELEASE         proper release with name"
 
-  VERSION may be either a tag like "IsabelleXXXX" that specifies the
-  release to be exported from the repository, or "-" to checkout the
-  current sources as an unofficial release.
+  Make Isabelle distribution from the main Mercurial repository at TUM.
 
-  NAME specifies an explicit distribution name, by default it is
-  derived from VERSION.
+  VERSION identifies the snapshot, using usual Mercurial terminology;
+  the default is RELEASE if given, otherwise "tip".
 
 EOF
   exit 1
@@ -51,131 +45,146 @@
 
 ## process command line
 
-[ "$#" -ne 1 -a "$#" -ne 2 ] && usage
+# options
 
-VERSION="$1"; shift
+RELEASE=""
 
-if [ "$#" -eq 0 ]; then
-  DISTNAME=""
-else
-  DISTNAME="$1"; shift
-fi
+while getopts "r:" OPT
+do
+  case "$OPT" in
+    r)
+      RELEASE="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+VERSION=""
+[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
+[ -z "$VERSION" ] && VERSION="$RELEASE"
+[ -z "$VERSION" ] && VERSION="tip"
+
+[ "$#" -gt 0 ] && usage
 
 
 ## main
 
-# dist version
+# tmp
+
+TMP="tmp-$USER$$"
+function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
+
+
+# retrieve archive and resolve version identifier
+
+mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
+cd "$DISTPREFIX/$TMP"
+
+echo "###"
+echo "### Retrieving Mercurial repository $VERSION"
+echo "###"
+
+{ wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
+  fail "Failed to retrieve $VERSION"
+
+IDENT=$(echo * | sed 's/isabelle-//')
+
+rm -f "isabelle-$IDENT/.hg_archival.txt"
+rm -f "isabelle-$IDENT/.hgtags"
+rm -f "isabelle-$IDENT/.hgignore"
+rm -f "isabelle-$IDENT/README_REPOSITORY"
+
+
+# dist name
 
 DATE=$(env LC_ALL=C date "+%d-%b-%Y")
 DISTDATE=$(env LC_ALL=C date "+%B %Y")
 
-if [ "$VERSION" = "-" ]; then
-  DISTIDENT="Isabelle_$DATE"
-  [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
-  DISTVERSION="$DISTNAME"
-  EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle"
-  UNOFFICIAL=true
+if [ -z "$RELEASE" ]; then
+  DISTNAME="Isabelle_$DATE"
+  DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
 else
-  DISTIDENT="$VERSION"
-  [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
+  DISTNAME="$RELEASE"
   DISTVERSION="$DISTNAME: $DISTDATE"
-  EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle"
-  UNOFFICIAL=""
 fi
 
 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
-mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!"
-[ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!"
-[ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!"
-
-
-# export repository
-
-echo "###"
-echo "### Exporting $DISTIDENT ..."
-echo "###"
+mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
+[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
+[ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; }
 
 cd "$DISTBASE"
+mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
+purge_tmp
 
-$EXPORT || fail "Export failed!"
+cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
+
+
+# website
 
-if [ -n "$CVS2CL" -a -n "$UNOFFICIAL" ]; then
-  cd $DISTNAME
-  $CVS2CL
-  gzip ChangeLog
-  cp ChangeLog.gz ..
-  cd ..
-fi
+mkdir -p ../website
+cat > ../website/distinfo.mak <<EOF
+# this is a generated file - do not edit unless you know what you are doing!
+DISTNAME=$DISTNAME
+DISTBASE=$DISTBASE
+EOF
 
-find . -name CVS -print | xargs rm -rf
+cp lib/html/library_index_content.template ../website/
+
+
+# prepare dist for release
+
+echo "###"
+echo "### Preparing distribution $DISTNAME"
+echo "###"
+
 find . -name .cvsignore -print | xargs rm -rf
 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x
 find . -print | xargs chmod u+rw
 
-
-# build components
-
-"$DISTBASE/$DISTNAME/Admin/build" all || fail "Failed to build distribution"
-
-
-# prepare dist dir for release
-
-echo "###"
-echo "### Preparing distribution ..."
-echo "###"
-
-cd "$DISTBASE/$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
-
-mkdir -p ../website
-cat > ../website/distinfo.mak <<EOF
-# this is a generated file - do not edit unless you know what you are doing!
+./Admin/build all || fail "Failed to build distribution"
+rm -rf Admin
 
-DISTNAME=$DISTNAME
-DISTIDENT=$DISTIDENT
-DISTBASE=$DISTBASE
-EOF
-
-cp Distribution/lib/html/library_index_content.template ../website/
+MOVE=$(find doc-src \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
+mv -f $MOVE doc
+rm doc/Isa-logics.eps
+rm doc/codegen_process.pdf
+rm -rf doc-src
 
-MOVE=$(find Doc \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
-mv -f $MOVE Distribution/doc
-rm Distribution/doc/Isa-logics.eps
-rm Distribution/doc/codegen_process.pdf
-rm -rf Doc
-
-mkdir src contrib
-mv $SRCS src
-
-mv Distribution/* .
-rmdir Distribution
-
+mkdir contrib
 
 cp doc/isabelle*.eps lib/logo
 
 
-if [ -n "$UNOFFICIAL" ]; then
+if [ -z "$RELEASE" ]; then
   {
     echo
     echo "IMPORTANT NOTE"
     echo "=============="
     echo
     echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
+    echo "See $REPOS/log/$IDENT for details."
     echo
   } >ANNOUNCE
 else
-  perl -pi -e "s/val is_official = false/val is_official = true/" src/Pure/ROOT.ML
+  perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
 fi
 
-perl -pi -e "s/ISABELLE_IDENTIFIER=\"\"/ISABELLE_IDENTIFIER=\"$DISTNAME\"/g;" lib/scripts/getsettings
-perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/library_index_header.template
-perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version
-perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README
+perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
+perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
+perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
+perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
+perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README
 
 
-rm -rf Admin
-
-
-# create archive
+# create archives
 
 echo "###"
 echo "### Creating archives ..."
@@ -184,6 +193,7 @@
 cd "$DISTBASE"
 
 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
+echo "$IDENT" >../ISABELLE_IDENT
 
 rm -f Isabelle
 ln -s "$DISTNAME" Isabelle
@@ -197,12 +207,10 @@
 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
 
 echo "$DISTNAME.tar.gz"
-tar cf "$DISTNAME.tar" Isabelle "$DISTNAME"
-gzip "$DISTNAME.tar"
+tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
 
 echo "${DISTNAME}_pdf.tar.gz"
-( cd pdf; tar cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
-gzip "${DISTNAME}_pdf.tar"
+tar -C pdf -czf "${DISTNAME}_pdf.tar.gz" "$DISTNAME"
 
 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
@@ -223,7 +231,3 @@
 
 rm -rf "${DISTNAME}-old"
 
-
-echo "###"
-echo "### Finished makedist."
-echo "###"
diff -r 128459bd72d2 -r 043a42ba2a4d Admin/makedist_mercurial
--- a/Admin/makedist_mercurial	Mon Dec 01 19:41:16 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,233 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-#
-# makedist_mercurial -- make Isabelle source distribution (via Mercurial)
-
-## global settings
-
-REPOS="http://isabelle.in.tum.de/repos/isabelle"
-
-DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
-
-umask 022
-
-
-## diagnostics
-
-PRG=$(basename "$0")
-THIS=$(cd $(dirname "$0"); echo "$PWD")
-
-function usage()
-{
-  cat <<EOF
-
-Usage: $PRG [OPTIONS] [VERSION]
-
-  Options are:
-    -r RELEASE         proper release with name"
-
-  Make Isabelle distribution from the main Mercurial repository at TUM.
-
-  VERSION identifies the snapshot, using usual Mercurial terminology;
-  the default is RELEASE if given, otherwise "tip".
-
-EOF
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-# options
-
-RELEASE=""
-
-while getopts "r:" OPT
-do
-  case "$OPT" in
-    r)
-      RELEASE="$OPTARG"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-VERSION=""
-[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
-[ -z "$VERSION" ] && VERSION="$RELEASE"
-[ -z "$VERSION" ] && VERSION="tip"
-
-[ "$#" -gt 0 ] && usage
-
-
-## main
-
-# tmp
-
-TMP="tmp-$USER$$"
-function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
-
-
-# retrieve archive and resolve version identifier
-
-mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
-cd "$DISTPREFIX/$TMP"
-
-echo "###"
-echo "### Retrieving Mercurial snapshot $VERSION"
-echo "###"
-
-{ wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
-  fail "Failed to retrieve $VERSION"
-
-IDENT=$(echo * | sed 's/isabelle-//')
-
-rm -f "isabelle-$IDENT/.hg_archival.txt"
-rm -f "isabelle-$IDENT/.hgtags"
-rm -f "isabelle-$IDENT/.hgignore"
-rm -f "isabelle-$IDENT/README_REPOSITORY"
-
-
-# dist name
-
-DATE=$(env LC_ALL=C date "+%d-%b-%Y")
-DISTDATE=$(env LC_ALL=C date "+%B %Y")
-
-if [ -z "$RELEASE" ]; then
-  DISTNAME="Isabelle_$DATE"
-  DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
-else
-  DISTNAME="$RELEASE"
-  DISTVERSION="$DISTNAME: $DISTDATE"
-fi
-
-DISTBASE="$DISTPREFIX/dist-$DISTNAME"
-mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
-[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
-[ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; }
-
-cd "$DISTBASE"
-mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
-purge_tmp
-
-cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
-
-
-# website
-
-mkdir -p ../website
-cat > ../website/distinfo.mak <<EOF
-# this is a generated file - do not edit unless you know what you are doing!
-DISTNAME=$DISTNAME
-DISTBASE=$DISTBASE
-EOF
-
-cp lib/html/library_index_content.template ../website/
-
-
-# prepare dist for release
-
-echo "###"
-echo "### Preparing distribution $DISTNAME"
-echo "###"
-
-find . -name .cvsignore -print | xargs rm -rf
-find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x
-find . -print | xargs chmod u+rw
-
-./Admin/build all || fail "Failed to build distribution"
-rm -rf Admin
-
-MOVE=$(find doc-src \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
-mv -f $MOVE doc
-rm doc/Isa-logics.eps
-rm doc/codegen_process.pdf
-rm -rf doc-src
-
-mkdir contrib
-
-cp doc/isabelle*.eps lib/logo
-
-
-if [ -z "$RELEASE" ]; then
-  {
-    echo
-    echo "IMPORTANT NOTE"
-    echo "=============="
-    echo
-    echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
-    echo "See $REPOS/log/$IDENT for details."
-    echo
-  } >ANNOUNCE
-else
-  perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
-fi
-
-perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
-perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
-perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
-perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
-perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README
-
-
-# create archives
-
-echo "###"
-echo "### Creating archives ..."
-echo "###"
-
-cd "$DISTBASE"
-
-echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
-echo "$IDENT" >../ISABELLE_IDENT
-
-rm -f Isabelle
-ln -s "$DISTNAME" Isabelle
-
-chown -R "$LOGNAME" "$DISTNAME"
-chmod -R u+w "$DISTNAME"
-chmod -R g=o "$DISTNAME"
-chgrp -R isabelle "$DISTNAME" Isabelle
-
-mkdir -p "pdf/$DISTNAME/doc"
-mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
-
-echo "$DISTNAME.tar.gz"
-tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
-
-echo "${DISTNAME}_pdf.tar.gz"
-tar -C pdf -czf "${DISTNAME}_pdf.tar.gz" "$DISTNAME"
-
-mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
-rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
-
-
-# cleanup dist
-
-mv "$DISTNAME" "${DISTNAME}-old"
-mkdir "$DISTNAME"
-
-mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
-  "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
-  "$DISTNAME"
-mkdir "$DISTNAME/doc"
-mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
-
-chgrp -R isabelle "$DISTNAME"
-
-rm -rf "${DISTNAME}-old"
-
diff -r 128459bd72d2 -r 043a42ba2a4d src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 19:41:16 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 19:42:26 2008 +0100
@@ -157,11 +157,6 @@
   show ?t by (rule x [OF `?a`])
 qed
 
-lemma
-  assumes "P <-> P" (is "?p <-> _")
-  shows "?p <-> ?p"
-  .
-
 
 text {* Interpretation between locales: sublocales *}
 
diff -r 128459bd72d2 -r 043a42ba2a4d src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Dec 01 19:41:16 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Dec 01 19:42:26 2008 +0100
@@ -304,12 +304,10 @@
     (* Type inference *)
     val (inst_cs' :: css', ctxt') =
       (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
-    (* Re-check to resolve bindings, elements and conclusion only *)
-    val (css'', _) = (fold_burrow o fold_burrow) check css' ctxt';
-    val (elem_css'', [concl_cs'']) = chop (length elem_css) css'';
+    val (elem_css', [concl_cs']) = chop (length elem_css) css';
   in
-    (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css''),
-      concl_cs'', ctxt')
+    (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css'),
+      concl_cs', ctxt')
   end;
 
 end;