# HG changeset patch
# User wenzelm
# Date 1259921940 -3600
# Node ID e4890d7bd9f8bba03ad1302c766f7ce12a986ae8
# Parent  dbc1a5b94449334d7be9cf02df76df604fb2d82e# Parent  99b52900aec0656d06472b9c5263400fd961a633
merged

diff -r dbc1a5b94449 -r e4890d7bd9f8 .hgtags
--- a/.hgtags	Fri Dec 04 11:04:07 2009 +0100
+++ b/.hgtags	Fri Dec 04 11:19:00 2009 +0100
@@ -24,6 +24,4 @@
 f9eb0f819642b2ad77119dbf8935bf13248f205d Isabelle94
 fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
 5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009
-9db7854eafc75143cda2509a5325eb9150331866 isa2009-1-test
-9db7854eafc75143cda2509a5325eb9150331866 isa2009-1-test
-4328de748fb2ceffe4ad5a6d5fbf3347f6aecfa6 isa2009-1-test
+6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1
diff -r dbc1a5b94449 -r e4890d7bd9f8 ANNOUNCE
--- a/ANNOUNCE	Fri Dec 04 11:04:07 2009 +0100
+++ b/ANNOUNCE	Fri Dec 04 11:19:00 2009 +0100
@@ -26,11 +26,16 @@
 
 * HOL: various parts of multivariate analysis.
 
+* HOL-Library: proof method "sos" (sum of squares) for nonlinear real
+arithmetic, based on external semidefinite programming solvers.
+
 * HOLCF: new definitional domain package.
 
 * Revised tutorial on locales.
 
-* Support for Poly/ML 5.3.0, with improved reporting of compiler
+* ML: tacticals for subgoal focus.
+
+* ML: support for Poly/ML 5.3.0, with improved reporting of compiler
 errors and run-time exceptions, including detailed source positions.
 
 * Parallel checking of nested Isar proofs, with improved scalability
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/MacOS/App1/script
--- a/Admin/MacOS/App1/script	Fri Dec 04 11:04:07 2009 +0100
+++ b/Admin/MacOS/App1/script	Fri Dec 04 11:19:00 2009 +0100
@@ -48,8 +48,9 @@
   /Applications/Emacs.app/Contents/MacOS/Emacs \
   "")"
 
+declare -a EMACS_OPTIONS=()
 if [ -n "$PROOFGENERAL_EMACS" ]; then
-  EMACS_OPTIONS="-p $PROOFGENERAL_EMACS"
+  EMACS_OPTIONS=(-p "$PROOFGENERAL_EMACS")
 fi
 
 
@@ -57,7 +58,7 @@
 
 OUTPUT="/tmp/isabelle$$.out"
 
-( "$ISABELLE_TOOL" emacs $EMACS_OPTIONS "$@" ) > "$OUTPUT" 2>&1
+( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
 RC=$?
 
 if [ "$RC" != 0 ]; then
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/ProofGeneral/interface
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/interface	Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,262 @@
+#!/usr/bin/env bash
+#
+# interface,v 9.1 2008/02/06 15:40:45 makarius Exp
+#
+# Proof General interface wrapper for Isabelle.
+
+
+## self references
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+SUPER="$(cd "$THIS/.."; pwd)"
+
+
+## diagnostics
+
+usage()
+{
+  echo
+  echo "Usage: Isabelle [OPTIONS] [FILES ...]"
+  echo
+  echo "  Options are:"
+  echo "    -I BOOL      use Isabelle/Isar (default: true, implied by -P true)"
+  echo "    -L NAME      abbreviates -l NAME -k NAME"
+  echo "    -P BOOL      actually start Proof General (default true), otherwise"
+  echo "                 run plain tty session"
+  echo "    -U BOOL      enable Unicode (UTF-8) communication (default true)"
+  echo "    -X BOOL      configure the X-Symbol package on startup (default true)"
+  echo "    -f SIZE      set X-Symbol font size (default 12)"
+  echo "    -g GEOMETRY  specify Emacs geometry"
+  echo "    -k NAME      use specific isar-keywords for named logic"
+  echo "    -l NAME      logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
+  echo "    -m MODE      add print mode for output"
+  echo "    -p NAME      Emacs program name (default emacs)"
+  echo "    -u BOOL      use personal .emacs file (default true)"
+  echo "    -w BOOL      use window system (default true)"
+  echo "    -x BOOL      enable the X-Symbol package on startup (default false)"
+  echo
+  echo "Starts Proof General for Isabelle with theory and proof FILES"
+  echo "(default Scratch.thy)."
+  echo
+  echo "  PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS"
+  echo
+  exit 1
+}
+
+fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+# options
+
+ISABELLE_OPTIONS=""
+ISAR="true"
+START_PG="true"
+GEOMETRY=""
+KEYWORDS=""
+LOGIC="$ISABELLE_LOGIC"
+PROGNAME="emacs"
+INITFILE="true"
+WINDOWSYSTEM="true"
+XSYMBOL=""
+XSYMBOL_SETUP=true
+XSYMBOL_FONTSIZE="12"
+UNICODE=""
+
+getoptions()
+{
+  OPTIND=1
+  while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT
+  do
+    case "$OPT" in
+      I)
+        ISAR="$OPTARG"
+        ;;
+      L)
+        KEYWORDS="$OPTARG"
+        LOGIC="$OPTARG"
+        ;;
+      P)
+        START_PG="$OPTARG"
+        ;;
+      U)
+        UNICODE="$OPTARG"
+        ;;
+      X)
+        XSYMBOL_SETUP="$OPTARG"
+        ;;
+      f)
+        XSYMBOL_FONTSIZE="$OPTARG"
+        ;;
+      g)
+        GEOMETRY="$OPTARG"
+        ;;
+      k)
+        KEYWORDS="$OPTARG"
+        ;;
+      l)
+        LOGIC="$OPTARG"
+        ;;
+      m)
+        if [ -z "$ISABELLE_OPTIONS" ]; then
+          ISABELLE_OPTIONS="-m $OPTARG"
+        else
+          ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
+        fi
+        ;;
+      p)
+        PROGNAME="$OPTARG"
+        ;;
+      u)
+        INITFILE="$OPTARG"
+        ;;
+      w)
+        WINDOWSYSTEM="$OPTARG"
+        ;;
+      x)
+        XSYMBOL="$OPTARG"
+        ;;
+      \?)
+        usage
+        ;;
+    esac
+  done
+}
+
+eval "OPTIONS=($PROOFGENERAL_OPTIONS)"
+getoptions "${OPTIONS[@]}"
+
+getoptions "$@"
+shift $(($OPTIND - 1))
+
+
+# args
+
+declare -a FILES=()
+
+if [ "$#" -eq 0 ]; then
+  FILES["${#FILES[@]}"]="Scratch.thy"
+else
+  while [ "$#" -gt 0 ]; do
+    FILES["${#FILES[@]}"]="$1"
+    shift
+  done
+fi
+
+
+## smart X11 font installation
+
+function checkfonts ()
+{
+  XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1
+
+  case "$XLSFONTS" in
+    xlsfonts:*)
+      return 1
+      ;;
+  esac
+
+  return 0
+}
+
+function installfonts ()
+{
+  checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
+}
+
+
+## main
+
+# Isabelle2008 compatibility
+[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE"
+[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL"
+
+if [ "$START_PG" = false ]; then
+
+  [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
+  exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
+
+else
+
+  declare -a ARGS=()
+
+  if [ -n "$GEOMETRY" ]; then
+    ARGS["${#ARGS[@]}"]="-geometry"
+    ARGS["${#ARGS[@]}"]="$GEOMETRY"
+  fi
+
+  [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q"
+
+  if [ "$WINDOWSYSTEM" = false ]; then
+    ARGS["${#ARGS[@]}"]="-nw"
+    XSYMBOL=false
+  elif [ -z "$DISPLAY" ]; then
+    XSYMBOL=false
+  else
+    [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts
+  fi
+
+  if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ]
+  then
+    if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ]
+    then
+      cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/"
+      cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/"
+      sleep 3
+    fi
+  fi
+
+  ARGS["${#ARGS[@]}"]="-l"
+  ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el"
+
+  if [ -n "$KEYWORDS" ]; then
+    if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
+      ARGS["${#ARGS[@]}"]="-l"
+      ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el"
+    elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
+      ARGS["${#ARGS[@]}"]="-l"
+      ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el"
+    else
+      fail "No isar-keywords file for '$KEYWORDS'"
+    fi
+  elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
+    ARGS["${#ARGS[@]}"]="-l"
+    ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el"
+  elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
+    ARGS["${#ARGS[@]}"]="-l"
+    ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el"
+  fi
+
+  for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
+      "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
+  do
+    if [ -f "$FILE" ]; then
+      ARGS["${#ARGS[@]}"]="-l"
+      ARGS["${#ARGS[@]}"]="$FILE"
+    fi
+  done
+
+  case "$LOGIC" in
+    /*)
+      ;;
+    */*)
+      LOGIC="$(pwd -P)/$LOGIC"
+      ;;
+  esac
+
+  export PROOFGENERAL_HOME="$SUPER"
+  export PROOFGENERAL_ASSISTANTS="isar"
+  export PROOFGENERAL_LOGIC="$LOGIC"
+  export PROOFGENERAL_XSYMBOL="$XSYMBOL"
+  export PROOFGENERAL_UNICODE="$UNICODE"
+
+  export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
+
+  exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"
+
+fi
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/ProofGeneral/isar-antiq-regexp.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/isar-antiq-regexp.patch	Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,21 @@
+--- a/isar/isar-syntax.el	Wed Aug 06 11:43:47 2008 +0200
++++ b/isar/isar-syntax.el	Thu Sep 18 15:21:16 2008 +0200
+@@ -252,14 +252,9 @@
+ 
+ ;; antiquotations
+ 
+-;; the \{0,10\} bound is there because otherwise font-lock sometimes hangs for
+-;; incomplete antiquotations like @{text bla"} (even though it is supposed to
+-;; stop at eol anyway).
+-
+-(defconst isar-antiq-regexp
+-  (concat "@{\\(?:[^\"{}]+\\|" isar-string "\\)\\{0,10\\}}")
+-  "Regexp matching Isabelle/Isar antiquoations.")
+-
++(defconst isar-antiq-regexp 
++  (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}") 
++  "Regexp matching Isabelle/Isar antiquotations.")
+ 
+ ;; keyword nesting
+ 
+
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/ProofGeneral/menu.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/menu.patch	Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,30 @@
+--- a/isar/isar.el	2008-07-10 20:47:49.000000000 +0200
++++ b/isar/isar.el	2009-11-26 20:51:44.103016094 +0100
+@@ -339,9 +339,12 @@
+      (error "Aborted."))
+   [(control p)])
+ 
+-(proof-definvisible isar-cmd-refute	"refute" [r])
+ (proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)])
++(proof-definvisible isar-cmd-nitpick "nitpick" [(control n)])
++(proof-definvisible isar-cmd-refute "refute" [r])
+ (proof-definvisible isar-cmd-sledgehammer "sledgehammer" [(control s)])
++(proof-definvisible isar-cmd-atp-kill "atp_kill")
++(proof-definvisible isar-cmd-atp-info "atp_info")
+ 
+ (defpgdefault menu-entries
+   (append
+@@ -349,9 +352,12 @@
+    (list
+     (cons "Commands"
+           (list
+-           ["refute"             isar-cmd-refute         t]
+            ["quickcheck"         isar-cmd-quickcheck     t]
++           ["nitpick"            isar-cmd-nitpick        t]
++           ["refute"             isar-cmd-refute         t]
+            ["sledgehammer"       isar-cmd-sledgehammer   t]
++	   ["sledgehammer: kill" isar-cmd-atp-kill       t]
++	   ["sledgehammer: info" isar-cmd-atp-info       t]
+ 	   ["display draft"	 isar-cmd-display-draft  t])))
+    (list
+     (cons "Show me ..."
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/ProofGeneral/progname.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/progname.patch	Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,89 @@
+--- a/isar/isabelle-system.el	2008-07-17 00:37:36.000000000 +0200
++++ b/isar/isabelle-system.el	2009-11-30 17:06:05.508481278 +0100
+@@ -97,8 +97,8 @@
+   (if (or proof-rsh-command
+ 	  (file-executable-p isa-isatool-command))
+       (let ((setting (isa-shell-command-to-string
+-		      (concat isa-isatool-command
+-			      " getenv -b " envvar))))
++		      (concat "\"" isa-isatool-command
++			      "\" getenv -b " envvar))))
+ 	(if (string-equal setting "")
+ 	    default
+ 	  setting))
+@@ -125,15 +125,12 @@
+   :type 'file
+   :group 'isabelle)
+ 
+-(defvar isabelle-prog-name nil
+-  "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
+-
+ (defun isa-tool-list-logics ()
+   "Generate a list of available object logics."
+   (if (isa-set-isatool-command)
+       (delete "" (split-string
+ 		  (isa-shell-command-to-string
+-		   (concat isa-isatool-command " findlogics")) "[ \t]"))))
++		   (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]"))))
+ 
+ (defcustom isabelle-logics-available nil
+   "*List of logics available to use with Isabelle.
+@@ -177,7 +174,7 @@
+ 
+ (defun isabelle-set-prog-name (&optional filename)
+   "Make proper command line for running Isabelle.
+-This function sets `isabelle-prog-name' and `proof-prog-name'."
++This function sets `proof-prog-name' and `isar-prog-args'."
+   (let*
+       ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
+       ;; under the interface wrapper script) indicate command line
+@@ -187,21 +184,20 @@
+ 		  (getenv "ISABELLE")	  ; command line override 
+ 		  (isa-getenv "ISABELLE") ; choose to match isatool
+ 		  "isabelle"))		  ; to 
+-       (isabelle-opts (getenv "ISABELLE_OPTIONS"))
+-       (opts (concat " -PI"  ;; Proof General + Isar
+-	      (if proof-shell-unicode " -m PGASCII" "")
+-	      (if (and isabelle-opts (not (equal isabelle-opts "")))
+-		  (concat " " isabelle-opts) "")))
++       (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
++       (opts (append (list "-PI")  ;; Proof General + Isar
++		     (if proof-shell-unicode (list "-m" "PGASCII") nil)
++		     isabelle-opts))
+        (logic (or isabelle-chosen-logic
+ 		  (getenv "PROOFGENERAL_LOGIC")))
+        (logicarg (if (and logic (not (equal logic "")))
+-		     (concat " " logic) "")))
++		     (list logic) nil)))
+     (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
+-    (setq isabelle-prog-name (concat isabelle opts logicarg))
+-    (setq proof-prog-name isabelle-prog-name)))
++    (setq isar-prog-args (append opts logicarg))
++    (setq proof-prog-name isabelle)))
+ 
+ (defun isabelle-choose-logic (logic)
+-  "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
++  "Adjust proof-prog-name and isar-prog-args for running LOGIC."
+   (interactive
+    (list (completing-read
+ 	  "Use logic: "
+@@ -224,9 +220,7 @@
+   (if (isa-set-isatool-command)
+       (apply 'start-process
+ 	     "isa-view-doc" nil
+-	     (append (split-string
+-		      isa-isatool-command) 
+-		     (list "doc" docname)))))
++	     (list isa-isatool-command "doc" docname))))
+ 
+ (defun isa-tool-list-docs ()
+   "Generate a list of documentation files available, with descriptions.
+@@ -236,7 +230,7 @@
+ passed to isa-tool-doc-command, DOCNAME will be viewed."
+   (if (isa-set-isatool-command)
+       (let ((docs (isa-shell-command-to-string
+-		   (concat isa-isatool-command " doc"))))
++		   (concat "\"" isa-isatool-command "\" doc"))))
+ 	(unless (string-equal docs "")
+ 	  (mapcan
+ 	   (function (lambda (docdes)
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/ProofGeneral/timeout.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/timeout.patch	Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,11 @@
+--- a/generic/proof-config.el	2008-07-21 18:37:10.000000000 +0200
++++ b/generic/proof-config.el	2009-11-29 17:41:37.409062091 +0100
+@@ -1493,7 +1493,7 @@
+    :type '(choice string (const nil))
+    :group 'proof-shell)
+ 
+-(defcustom proof-shell-quit-timeout 4
++(defcustom proof-shell-quit-timeout 45
+   ;; FIXME could add option to quiz user before rude kill.
+   "The number of seconds to wait after sending proof-shell-quit-cmd.
+ After this timeout, the proof shell will be killed off more rudely.
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/ProofGeneral/version.patch
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/version.patch	Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,20 @@
+--- a/generic/proof-site.el	2008-07-23 14:40:14.000000000 +0200
++++ b/generic/proof-site.el	2009-11-28 16:13:56.409505412 +0100
+@@ -55,7 +55,7 @@
+ 
+ (eval-and-compile
+ ;; WARNING: do not edit next line (constant is edited in Makefile.devel)
+-  (defconst proof-general-version "Proof General Version 3.7.1. Released by da on Wed 23 Jul 2008."
++  (defconst proof-general-version "Proof General Version 3.7.1.1. Fabricated by makarius on Mon 30 Nov 2009."
+     "Version string identifying Proof General release."))
+ 
+ (defconst proof-general-short-version 
+@@ -64,7 +64,7 @@
+       (string-match "Version \\([^ ]+\\)\\." proof-general-version)
+       (match-string 1 proof-general-version))))
+ 
+-(defconst proof-general-version-year "2008")
++(defconst proof-general-version-year "2009")
+ 
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+ ;;
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/isatest/settings/at-poly-5.1-para-e
--- a/Admin/isatest/settings/at-poly-5.1-para-e	Fri Dec 04 11:04:07 2009 +0100
+++ b/Admin/isatest/settings/at-poly-5.1-para-e	Fri Dec 04 11:19:00 2009 +0100
@@ -22,6 +22,6 @@
 ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 20"
+ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 10"
 
 HOL_USEDIR_OPTIONS="-p 2 -q 0"
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/makebin
--- a/Admin/makebin	Fri Dec 04 11:04:07 2009 +0100
+++ b/Admin/makebin	Fri Dec 04 11:19:00 2009 +0100
@@ -109,6 +109,8 @@
   touch "heaps/$COMPILER/log/HOL.gz"
   touch "heaps/$COMPILER/HOL-Nominal"
   touch "heaps/$COMPILER/log/HOL-Nominal.gz"
+  touch "heaps/$COMPILER/HOLCF"
+  touch "heaps/$COMPILER/log/HOLCF.gz"
   touch "heaps/$COMPILER/ZF"
   touch "heaps/$COMPILER/log/ZF.gz"
   mkdir browser_info
@@ -116,6 +118,7 @@
   ./build -bait
 else
   ./build -b -m HOL-Nominal HOL
+  ./build -b HOLCF
   ./build -b ZF
   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
 fi
@@ -133,7 +136,7 @@
     gzip -f "${ISABELLE_NAME}_library.tar"
     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
 else
-  for IMG in HOL HOL-Nominal ZF
+  for IMG in HOL HOL-Nominal HOLCF ZF
   do
     tar cf "${IMG}_$PLATFORM.tar" \
       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/makebundle
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/makebundle	Fri Dec 04 11:19:00 2009 +0100
@@ -0,0 +1,75 @@
+#!/usr/bin/env bash
+#
+# makebundle -- re-package with add-on components
+
+## global settings
+
+TMP="/var/tmp/isabelle-makebundle$$"
+
+
+## diagnostics
+
+PRG=$(basename "$0")
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG ARCHIVE COMPONENTS"
+  echo
+  echo "  Re-package Isabelle distribution with add-on components."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+[ "$#" -lt 1 ] && usage
+
+ARCHIVE="$1"; shift
+
+declare -a COMPONENTS
+COMPONENTS=("$@")
+
+
+## main
+
+mkdir "$TMP" || fail "Cannot create directory $TMP"
+
+ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
+ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
+ISABELLE_HOME="$TMP/$ISABELLE_NAME"
+
+[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
+tar -C "$TMP" -x -z -f "$ARCHIVE"
+
+echo "#bundled components" >> "$ISABELLE_HOME/etc/components"
+
+for COMPONENT in "${COMPONENTS[@]}"
+do
+  tar -C "$ISABELLE_HOME/contrib" -x -z -f "$COMPONENT"
+  NAME="$(basename "$COMPONENT" .tar.gz)"
+  [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $COMPONENT"
+
+  if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then
+    echo "component $NAME"
+    echo "contrib/$NAME" >> "$ISABELLE_HOME/etc/components"
+  else
+    echo "package $NAME"
+  fi
+done
+
+tar -C "$TMP" -c -z \
+  -f "${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle.tar.gz" \
+  Isabelle "$ISABELLE_NAME"
+
+
+# clean up
+cd /tmp
+rm -rf "$TMP"
diff -r dbc1a5b94449 -r e4890d7bd9f8 Admin/makedist
--- a/Admin/makedist	Fri Dec 04 11:04:07 2009 +0100
+++ b/Admin/makedist	Fri Dec 04 11:19:00 2009 +0100
@@ -4,7 +4,8 @@
 
 ## global settings
 
-REPOS="http://isabelle.in.tum.de/repos/isabelle"
+REPOS_NAME="isabelle-release"
+REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}"
 
 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
 
@@ -92,12 +93,12 @@
 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
   fail "Failed to retrieve $VERSION"
 
-IDENT=$(echo * | sed 's/isabelle-//')
+IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
 
-rm -f "isabelle-$IDENT/.hg_archival.txt"
-rm -f "isabelle-$IDENT/.hgtags"
-rm -f "isabelle-$IDENT/.hgignore"
-rm -f "isabelle-$IDENT/README_REPOSITORY"
+rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
+rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
+rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
+rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
 
 
 # dist name
@@ -118,7 +119,7 @@
 [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
 
 cd "$DISTBASE"
-mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
+mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
 purge_tmp
 
 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
diff -r dbc1a5b94449 -r e4890d7bd9f8 bin/isabelle
--- a/bin/isabelle	Fri Dec 04 11:04:07 2009 +0100
+++ b/bin/isabelle	Fri Dec 04 11:19:00 2009 +0100
@@ -30,7 +30,7 @@
   echo "  Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
   echo
   echo "  Available tools are:"
-  for DIR in ${TOOLS[@]}
+  for DIR in "${TOOLS[@]}"
   do
     if [ -d "$DIR" ]; then
       for TOOL in "$DIR"/*
diff -r dbc1a5b94449 -r e4890d7bd9f8 bin/isabelle-process
--- a/bin/isabelle-process	Fri Dec 04 11:04:07 2009 +0100
+++ b/bin/isabelle-process	Fri Dec 04 11:19:00 2009 +0100
@@ -181,7 +181,9 @@
 
 case "$OUTPUT" in
   "")
-    [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
+    if [ -z "$READONLY" -a -w "$INFILE" ]; then
+      perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
+    fi
     ;;
   */*)
     OUTFILE="$OUTPUT"
diff -r dbc1a5b94449 -r e4890d7bd9f8 doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Fri Dec 04 11:04:07 2009 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex	Fri Dec 04 11:19:00 2009 +0100
@@ -1260,7 +1260,7 @@
 \hspace*{0pt}\\
 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
 \hspace*{0pt}\\
-\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int)\\
+\hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int);\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\
 \hspace*{0pt}\\
@@ -1285,7 +1285,7 @@
 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\
 \hspace*{0pt}\\
 \hspace*{0pt}val example :~IntInf.int =\\
-\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int)\\
+\hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int);\\
 \hspace*{0pt}\\
 \hspace*{0pt}end;~(*struct Example*)%
 \end{isamarkuptext}%
diff -r dbc1a5b94449 -r e4890d7bd9f8 doc-src/Codegen/Thy/Program.thy
--- a/doc-src/Codegen/Thy/Program.thy	Fri Dec 04 11:04:07 2009 +0100
+++ b/doc-src/Codegen/Thy/Program.thy	Fri Dec 04 11:19:00 2009 +0100
@@ -430,5 +430,220 @@
   likely to be used in such situations.
 *}
 
+subsection {* Inductive Predicates *}
+(*<*)
+hide const append
+
+inductive append
+where
+  "append [] ys ys"
+| "append xs ys zs ==> append (x # xs) ys (x # zs)"
+(*>*)
+text {*
+To execute inductive predicates, a special preprocessor, the predicate
+ compiler, generates code equations from the introduction rules of the predicates.
+The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
+Consider the simple predicate @{const append} given by these two
+introduction rules:
+*}
+text %quote {*
+@{thm append.intros(1)[of ys]}\\
+\noindent@{thm append.intros(2)[of xs ys zs x]}
+*}
+text {*
+\noindent To invoke the compiler, simply use @{command_def "code_pred"}:
+*}
+code_pred %quote append .
+text {*
+\noindent The @{command "code_pred"} command takes the name
+of the inductive predicate and then you put a period to discharge
+a trivial correctness proof. 
+The compiler infers possible modes 
+for the predicate and produces the derived code equations.
+Modes annotate which (parts of the) arguments are to be taken as input,
+and which output. Modes are similar to types, but use the notation @{text "i"}
+for input and @{text "o"} for output.
+ 
+For @{term "append"}, the compiler can infer the following modes:
+\begin{itemize}
+\item @{text "i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool"}
+\item @{text "i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}
+\item @{text "o \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool"}
+\end{itemize}
+You can compute sets of predicates using @{command_def "values"}:
+*}
+values %quote "{zs. append [(1::nat),2,3] [4,5] zs}"
+text {* \noindent outputs @{text "{[1, 2, 3, 4, 5]}"}, and *}
+values %quote "{(xs, ys). append xs ys [(2::nat),3]}"
+text {* \noindent outputs @{text "{([], [2, 3]), ([2], [3]), ([2, 3], [])}"}. *}
+text {*
+\noindent If you are only interested in the first elements of the set
+comprehension (with respect to a depth-first search on the introduction rules), you can
+pass an argument to
+@{command "values"} to specify the number of elements you want:
+*}
+
+values %quote 1 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
+values %quote 3 "{(xs, ys). append xs ys [(1::nat),2,3,4]}"
+
+text {*
+\noindent The @{command "values"} command can only compute set
+ comprehensions for which a mode has been inferred.
+
+The code equations for a predicate are made available as theorems with
+ the suffix @{text "equation"}, and can be inspected with:
+*}
+thm %quote append.equation
+text {*
+\noindent More advanced options are described in the following subsections.
+*}
+subsubsection {* Alternative names for functions *}
+text {* 
+By default, the functions generated from a predicate are named after the predicate with the
+mode mangled into the name (e.g., @{text "append_i_i_o"}).
+You can specify your own names as follows:
+*}
+code_pred %quote (modes: i => i => o => bool as concat,
+  o => o => i => bool as split,
+  i => o => i => bool as suffix) append .
+
+subsubsection {* Alternative introduction rules *}
+text {*
+Sometimes the introduction rules of an predicate are not executable because they contain
+non-executable constants or specific modes could not be inferred.
+It is also possible that the introduction rules yield a function that loops forever
+due to the execution in a depth-first search manner.
+Therefore, you can declare alternative introduction rules for predicates with the attribute
+@{attribute "code_pred_intro"}.
+For example, the transitive closure is defined by: 
+*}
+text %quote {*
+@{thm tranclp.intros(1)[of r a b]}\\
+\noindent @{thm tranclp.intros(2)[of r a b c]}
+*}
+text {*
+\noindent These rules do not suit well for executing the transitive closure 
+with the mode @{text "(i \<Rightarrow> o \<Rightarrow> bool) \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool"}, as the second rule will
+cause an infinite loop in the recursive call.
+This can be avoided using the following alternative rules which are
+declared to the predicate compiler by the attribute @{attribute "code_pred_intro"}:
+*}
+lemma %quote [code_pred_intro]:
+  "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
+  "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
+by auto
+text {*
+\noindent After declaring all alternative rules for the transitive closure,
+you invoke @{command "code_pred"} as usual.
+As you have declared alternative rules for the predicate, you are urged to prove that these
+introduction rules are complete, i.e., that you can derive an elimination rule for the
+alternative rules:
+*}
+code_pred %quote tranclp
+proof -
+  case tranclp
+  from this converse_tranclpE[OF this(1)] show thesis by metis
+qed
+text {*
+\noindent Alternative rules can also be used for constants that have not
+been defined inductively. For example, the lexicographic order which
+is defined as: *}
+text %quote {*
+@{thm [display] lexord_def[of "r"]}
+*}
+text {*
+\noindent To make it executable, you can derive the following two rules and prove the
+elimination rule:
+*}
+(*<*)
+lemma append: "append xs ys zs = (xs @ ys = zs)"
+by (induct xs arbitrary: ys zs) (auto elim: append.cases intro: append.intros)
+(*>*)
+lemma %quote [code_pred_intro]:
+  "append xs (a # v) ys \<Longrightarrow> lexord r (xs, ys)"
+(*<*)unfolding lexord_def Collect_def by (auto simp add: append)(*>*)
+
+lemma %quote [code_pred_intro]:
+  "append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b)
+  \<Longrightarrow> lexord r (xs, ys)"
+(*<*)unfolding lexord_def Collect_def append mem_def apply simp
+apply (rule disjI2) by auto
+(*>*)
+
+code_pred %quote lexord
+(*<*)
+proof -
+  fix r a1
+  assume lexord: "lexord r a1"
+  assume 1: "\<And> xs ys a v. a1 = (xs, ys) \<Longrightarrow> append xs (a # v) ys \<Longrightarrow> thesis"
+  assume 2: "\<And> xs ys u a v b w. a1 = (xs, ys) \<Longrightarrow> append u (a # v) xs \<Longrightarrow> append u (b # w) ys \<Longrightarrow> r (a, b) \<Longrightarrow> thesis"
+  obtain xs ys where a1: "a1 = (xs, ys)" by fastsimp
+  {
+    assume "\<exists>a v. ys = xs @ a # v"
+    from this 1 a1 have thesis
+        by (fastsimp simp add: append)
+  } moreover
+  {
+    assume "\<exists>u a b v w. (a, b) \<in> r \<and> xs = u @ a # v \<and> ys = u @ b # w"
+    from this 2 a1 have thesis by (fastsimp simp add: append mem_def)
+  } moreover
+  note lexord[simplified a1]
+  ultimately show thesis
+    unfolding lexord_def
+    by (fastsimp simp add: Collect_def)
+qed
+(*>*)
+subsubsection {* Options for values *}
+text {*
+In the presence of higher-order predicates, multiple modes for some predicate could be inferred
+that are not disambiguated by the pattern of the set comprehension.
+To disambiguate the modes for the arguments of a predicate, you can state
+the modes explicitly in the @{command "values"} command. 
+Consider the simple predicate @{term "succ"}:
+*}
+inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+where
+  "succ 0 (Suc 0)"
+| "succ x y \<Longrightarrow> succ (Suc x) (Suc y)"
+
+code_pred succ .
+
+text {*
+\noindent For this, the predicate compiler can infer modes @{text "o \<Rightarrow> o \<Rightarrow> bool"}, @{text "i \<Rightarrow> o \<Rightarrow> bool"},
+  @{text "o \<Rightarrow> i \<Rightarrow> bool"} and @{text "i \<Rightarrow> i \<Rightarrow> bool"}.
+The invocation of @{command "values"} @{text "{n. tranclp succ 10 n}"} loops, as multiple
+modes for the predicate @{text "succ"} are possible and here the first mode @{text "o \<Rightarrow> o \<Rightarrow> bool"}
+is chosen. To choose another mode for the argument, you can declare the mode for the argument between
+the @{command "values"} and the number of elements.
+*}
+values %quote [mode: i => o => bool] 20 "{n. tranclp succ 10 n}"
+values %quote [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
+
+subsubsection {* Embedding into functional code within Isabelle/HOL *}
+text {*
+To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
+you have a number of options:
+\begin{itemize}
+\item You want to use the first-order predicate with the mode
+  where all arguments are input. Then you can use the predicate directly, e.g.
+\begin{quote}
+  @{text "valid_suffix ys zs = "}\\
+  @{text "(if append [Suc 0, 2] ys zs then Some ys else None)"}
+\end{quote}
+\item If you know that the execution returns only one value (it is deterministic), then you can
+  use the combinator @{term "Predicate.the"}, e.g., a functional concatenation of lists
+  is defined with
+\begin{quote}
+  @{term "functional_concat xs ys = Predicate.the (append_i_i_o xs ys)"}
+\end{quote}
+  Note that if the evaluation does not return a unique value, it raises a run-time error
+  @{term "not_unique"}.
+\end{itemize}
+*}
+subsubsection {* Further Examples *}
+text {* Further examples for compiling inductive predicates can be found in
+the @{text "HOL/ex/Predicate_Compile_ex"} theory file.
+There are also some examples in the Archive of Formal Proofs, notably
+in the @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"} sessions.
+*}
 end
- 
\ No newline at end of file
diff -r dbc1a5b94449 -r e4890d7bd9f8 doc-src/Codegen/Thy/document/Program.tex
--- a/doc-src/Codegen/Thy/document/Program.tex	Fri Dec 04 11:04:07 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Program.tex	Fri Dec 04 11:19:00 2009 +0100
@@ -968,6 +968,458 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Inductive Predicates%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+To execute inductive predicates, a special preprocessor, the predicate
+ compiler, generates code equations from the introduction rules of the predicates.
+The mechanisms of this compiler are described in \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
+Consider the simple predicate \isa{append} given by these two
+introduction rules:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isa{append\ {\isacharbrackleft}{\isacharbrackright}\ ys\ ys}\\
+\noindent\isa{append\ xs\ ys\ zs\ {\isasymLongrightarrow}\ append\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys\ {\isacharparenleft}x\ {\isacharhash}\ zs{\isacharparenright}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent To invoke the compiler, simply use \indexdef{}{command}{code\_pred}\hypertarget{command.code-pred}{\hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} command takes the name
+of the inductive predicate and then you put a period to discharge
+a trivial correctness proof. 
+The compiler infers possible modes 
+for the predicate and produces the derived code equations.
+Modes annotate which (parts of the) arguments are to be taken as input,
+and which output. Modes are similar to types, but use the notation \isa{i}
+for input and \isa{o} for output.
+ 
+For \isa{append}, the compiler can infer the following modes:
+\begin{itemize}
+\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
+\item \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
+\item \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}
+\end{itemize}
+You can compute sets of predicates using \indexdef{}{command}{values}\hypertarget{command.values}{\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{values}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharbraceleft}zs{\isachardot}\ append\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}\ {\isacharbrackleft}{\isadigit{4}}{\isacharcomma}{\isadigit{5}}{\isacharbrackright}\ zs{\isacharbraceright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent outputs \isa{{\isacharbraceleft}{\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharbrackright}{\isacharbraceright}}, and%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{values}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{2}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{3}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent outputs \isa{{\isacharbraceleft}{\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isadigit{3}}{\isacharbrackright}{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isacharbraceright}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\noindent If you are only interested in the first elements of the set
+comprehension (with respect to a depth-first search on the introduction rules), you can
+pass an argument to
+\hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} to specify the number of elements you want:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{values}\isamarkupfalse%
+\ {\isadigit{1}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\isacommand{values}\isamarkupfalse%
+\ {\isadigit{3}}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardot}\ append\ xs\ ys\ {\isacharbrackleft}{\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharcomma}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{4}}{\isacharbrackright}{\isacharbraceright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command can only compute set
+ comprehensions for which a mode has been inferred.
+
+The code equations for a predicate are made available as theorems with
+ the suffix \isa{equation}, and can be inspected with:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{thm}\isamarkupfalse%
+\ append{\isachardot}equation%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent More advanced options are described in the following subsections.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Alternative names for functions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+By default, the functions generated from a predicate are named after the predicate with the
+mode mangled into the name (e.g., \isa{append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o}).
+You can specify your own names as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\ {\isacharparenleft}modes{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool\ as\ concat{\isacharcomma}\isanewline
+\ \ o\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ split{\isacharcomma}\isanewline
+\ \ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool\ as\ suffix{\isacharparenright}\ append\ \isacommand{{\isachardot}}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isamarkupsubsubsection{Alternative introduction rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Sometimes the introduction rules of an predicate are not executable because they contain
+non-executable constants or specific modes could not be inferred.
+It is also possible that the introduction rules yield a function that loops forever
+due to the execution in a depth-first search manner.
+Therefore, you can declare alternative introduction rules for predicates with the attribute
+\hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}.
+For example, the transitive closure is defined by:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b}\\
+\noindent \isa{{\isasymlbrakk}r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isacharsemicolon}\ r\ b\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent These rules do not suit well for executing the transitive closure 
+with the mode \isa{{\isacharparenleft}i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, as the second rule will
+cause an infinite loop in the recursive call.
+This can be avoided using the following alternative rules which are
+declared to the predicate compiler by the attribute \hyperlink{attribute.code-pred-intro}{\mbox{\isa{code{\isacharunderscore}pred{\isacharunderscore}intro}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c{\isachardoublequoteclose}\isanewline
+\isacommand{by}\isamarkupfalse%
+\ auto%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent After declaring all alternative rules for the transitive closure,
+you invoke \hyperlink{command.code-pred}{\mbox{\isa{\isacommand{code{\isacharunderscore}pred}}}} as usual.
+As you have declared alternative rules for the predicate, you are urged to prove that these
+introduction rules are complete, i.e., that you can derive an elimination rule for the
+alternative rules:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\ tranclp\isanewline
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \isacommand{case}\isamarkupfalse%
+\ tranclp\isanewline
+\ \ \isacommand{from}\isamarkupfalse%
+\ this\ converse{\isacharunderscore}tranclpE{\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
+\ thesis\ \isacommand{by}\isamarkupfalse%
+\ metis\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Alternative rules can also be used for constants that have not
+been defined inductively. For example, the lexicographic order which
+is defined as:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\begin{isabelle}%
+lexord\ r\ {\isasymequiv}\isanewline
+{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\isanewline
+\isaindent{\ }{\isasymexists}a\ v{\isachardot}\ y\ {\isacharequal}\ x\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymor}\isanewline
+\isaindent{\ {\isasymexists}a\ v{\isachardot}\ }{\isacharparenleft}{\isasymexists}u\ a\ b\ v\ w{\isachardot}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\ {\isasymand}\ x\ {\isacharequal}\ u\ {\isacharat}\ a\ {\isacharhash}\ v\ {\isasymand}\ y\ {\isacharequal}\ u\ {\isacharat}\ b\ {\isacharhash}\ w{\isacharparenright}{\isacharbraceright}%
+\end{isabelle}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent To make it executable, you can derive the following two rules and prove the
+elimination rule:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}append\ xs\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}append\ u\ {\isacharparenleft}a\ {\isacharhash}\ v{\isacharparenright}\ xs\ {\isasymLongrightarrow}\ append\ u\ {\isacharparenleft}b\ {\isacharhash}\ w{\isacharparenright}\ ys\ {\isasymLongrightarrow}\ r\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\isanewline
+\ \ {\isasymLongrightarrow}\ lexord\ r\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\ lexord%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isamarkupsubsubsection{Options for values%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In the presence of higher-order predicates, multiple modes for some predicate could be inferred
+that are not disambiguated by the pattern of the set comprehension.
+To disambiguate the modes for the arguments of a predicate, you can state
+the modes explicitly in the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} command. 
+Consider the simple predicate \isa{succ}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{inductive}\isamarkupfalse%
+\ succ\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}succ\ {\isadigit{0}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+{\isacharbar}\ {\isachardoublequoteopen}succ\ x\ y\ {\isasymLongrightarrow}\ succ\ {\isacharparenleft}Suc\ x{\isacharparenright}\ {\isacharparenleft}Suc\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}pred}\isamarkupfalse%
+\ succ%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent For this, the predicate compiler can infer modes \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}, \isa{i\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool},
+  \isa{o\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool} and \isa{i\ {\isasymRightarrow}\ i\ {\isasymRightarrow}\ bool}.
+The invocation of \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} \isa{{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}} loops, as multiple
+modes for the predicate \isa{succ} are possible and here the first mode \isa{o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ bool}
+is chosen. To choose another mode for the argument, you can declare the mode for the argument between
+the \hyperlink{command.values}{\mbox{\isa{\isacommand{values}}}} and the number of elements.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{values}\isamarkupfalse%
+\ {\isacharbrackleft}mode{\isacharcolon}\ i\ {\isacharequal}{\isachargreater}\ o\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{2}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ {\isadigit{1}}{\isadigit{0}}\ n{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\isacommand{values}\isamarkupfalse%
+\ {\isacharbrackleft}mode{\isacharcolon}\ o\ {\isacharequal}{\isachargreater}\ i\ {\isacharequal}{\isachargreater}\ bool{\isacharbrackright}\ {\isadigit{1}}{\isadigit{0}}\ {\isachardoublequoteopen}{\isacharbraceleft}n{\isachardot}\ tranclp\ succ\ n\ {\isadigit{1}}{\isadigit{0}}{\isacharbraceright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isamarkupsubsubsection{Embedding into functional code within Isabelle/HOL%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+To embed the computation of an inductive predicate into functions that are defined in Isabelle/HOL,
+you have a number of options:
+\begin{itemize}
+\item You want to use the first-order predicate with the mode
+  where all arguments are input. Then you can use the predicate directly, e.g.
+\begin{quote}
+  \isa{valid{\isacharunderscore}suffix\ ys\ zs\ {\isacharequal}}\\
+  \isa{{\isacharparenleft}if\ append\ {\isacharbrackleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{2}}{\isacharbrackright}\ ys\ zs\ then\ Some\ ys\ else\ None{\isacharparenright}}
+\end{quote}
+\item If you know that the execution returns only one value (it is deterministic), then you can
+  use the combinator \isa{Predicate{\isachardot}the}, e.g., a functional concatenation of lists
+  is defined with
+\begin{quote}
+  \isa{functional{\isacharunderscore}concat\ xs\ ys\ {\isacharequal}\ Predicate{\isachardot}the\ {\isacharparenleft}append{\isacharunderscore}i{\isacharunderscore}i{\isacharunderscore}o\ xs\ ys{\isacharparenright}}
+\end{quote}
+  Note that if the evaluation does not return a unique value, it raises a run-time error
+  \isa{not{\isacharunderscore}unique}.
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Further Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Further examples for compiling inductive predicates can be found in
+the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex} theory file.
+There are also some examples in the Archive of Formal Proofs, notably
+in the \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava} sessions.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isadelimtheory
 %
 \endisadelimtheory
@@ -982,7 +1434,7 @@
 %
 \endisadelimtheory
 \isanewline
-\ \end{isabellebody}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r dbc1a5b94449 -r e4890d7bd9f8 doc-src/Codegen/codegen.tex
--- a/doc-src/Codegen/codegen.tex	Fri Dec 04 11:04:07 2009 +0100
+++ b/doc-src/Codegen/codegen.tex	Fri Dec 04 11:19:00 2009 +0100
@@ -13,7 +13,7 @@
 
 \title{\includegraphics[scale=0.5]{isabelle_isar}
   \\[4ex] Code generation from Isabelle/HOL theories}
-\author{\emph{Florian Haftmann}}
+\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
 
 \begin{document}
 
diff -r dbc1a5b94449 -r e4890d7bd9f8 doc-src/manual.bib
--- a/doc-src/manual.bib	Fri Dec 04 11:04:07 2009 +0100
+++ b/doc-src/manual.bib	Fri Dec 04 11:19:00 2009 +0100
@@ -172,6 +172,14 @@
   title =        {Calculational reasoning revisited --- an {Isabelle/Isar} experience},
   crossref =     {tphols2001}}
 
+@inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL,
+    author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
+    booktitle = {Theorem Proving in Higher Order Logics},
+    pages = {131--146},
+    title = {Turning Inductive into Equational Specifications},
+    year = {2009}
+}
+
 @INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
   crossref        = "tphols2000",
   title           = "Proof terms for simply typed higher order logic",
diff -r dbc1a5b94449 -r e4890d7bd9f8 etc/settings
--- a/etc/settings	Fri Dec 04 11:04:07 2009 +0100
+++ b/etc/settings	Fri Dec 04 11:19:00 2009 +0100
@@ -208,21 +208,9 @@
 ## Set HOME only for tools you have installed!
 
 # External provers
-E_HOME=$(choosefrom \
-  "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \
-  "$ISABELLE_HOME/../E/$ML_PLATFORM" \
-  "/usr/local/E/$ML_PLATFORM" \
-  "")
-VAMPIRE_HOME=$(choosefrom \
-  "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
-  "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
-  "/usr/local/vampire/$ML_PLATFORM" \
-  "")
-SPASS_HOME=$(choosefrom \
-  "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \
-  "$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \
-  "/usr/local/spass/$ML_PLATFORM" \
-  "")
+#E_HOME=/usr/local/bin
+#SPASS_HOME=/usr/local/bin
+#VAMPIRE_HOME=/usr/local/bin
 
 # HOL4 proof objects (cf. Isabelle/src/HOL/Import)
 #HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
diff -r dbc1a5b94449 -r e4890d7bd9f8 lib/Tools/findlogics
--- a/lib/Tools/findlogics	Fri Dec 04 11:04:07 2009 +0100
+++ b/lib/Tools/findlogics	Fri Dec 04 11:19:00 2009 +0100
@@ -39,4 +39,4 @@
   done
 done
 
-echo $({ for L in ${LOGICS[@]}; do echo "$L"; done; } | sort | uniq)
+echo $({ for L in "${LOGICS[@]}"; do echo "$L"; done; } | sort | uniq)
diff -r dbc1a5b94449 -r e4890d7bd9f8 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Dec 04 11:04:07 2009 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Dec 04 11:19:00 2009 +0100
@@ -537,8 +537,8 @@
  fun token s =
   Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ")
  val numeral = Scan.one isnum
- val decimalint = Scan.repeat numeral >> (rat_of_string o implode)
- val decimalfrac = Scan.repeat numeral
+ val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
+ val decimalfrac = Scan.repeat1 numeral
     >> (fn s => rat_of_string(implode s) // pow10 (length s))
  val decimalsig =
     decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
diff -r dbc1a5b94449 -r e4890d7bd9f8 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Dec 04 11:04:07 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML	Fri Dec 04 11:19:00 2009 +0100
@@ -496,7 +496,7 @@
     else if ! ambiguity_is_error then error (ambiguity_msg pos)
     else
       (warning (cat_lines
-        (("Ambiguous input " ^ Position.str_of pos ^
+        (("Ambiguous input" ^ Position.str_of pos ^
           "\nproduces " ^ string_of_int len ^ " parse trees" ^
           (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
           map show_pt (Library.take (limit, pts)))));
diff -r dbc1a5b94449 -r e4890d7bd9f8 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Fri Dec 04 11:04:07 2009 +0100
+++ b/src/Pure/pure_setup.ML	Fri Dec 04 11:19:00 2009 +0100
@@ -39,6 +39,11 @@
 then use "ML-Systems/install_pp_polyml.ML"
 else ();
 
+if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
+  Secure.use_text ML_Parse.global_context (0, "") false
+    "PolyML.Compiler.maxInlineSize := 20"
+else ();
+
 
 (* ML toplevel use commands *)