# HG changeset patch
# User berghofe
# Date 1343063221 -7200
# Node ID 808a5ba619919c454986b639bf7f13b3e4c6e673
# Parent  2421ff8c57a597b9cd492a5b17d8c7a92ca79cf4# Parent  4ad6182d5bb990a4bbfa2379e1d5b78355735b03
merged

diff -r 2421ff8c57a5 -r 808a5ba61991 Admin/MacOS/App1/README
--- a/Admin/MacOS/App1/README	Mon Jul 23 18:52:10 2012 +0200
+++ b/Admin/MacOS/App1/README	Mon Jul 23 19:07:01 2012 +0200
@@ -5,5 +5,6 @@
 
 * CocoaDialog 2.1.1 http://cocoadialog.sourceforge.net/
 
-* Platypus 4.0 http://www.sveinbjorn.org/platypus
+* Platypus 4.7 http://www.sveinbjorn.org/platypus
+  Preferences: Install command line tool
 
diff -r 2421ff8c57a5 -r 808a5ba61991 Admin/MacOS/App1/mk
--- a/Admin/MacOS/App1/mk	Mon Jul 23 18:52:10 2012 +0200
+++ b/Admin/MacOS/App1/mk	Mon Jul 23 19:07:01 2012 +0200
@@ -4,15 +4,17 @@
 
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
-PLATYPUS_APP="/Applications/Platypus-4.0/Platypus.app"
 COCOADIALOG_APP="/Applications/CocoaDialog.app"
 
-"$PLATYPUS_APP/Contents/Resources/platypus" \
+/usr/local/bin/platypus \
   -a Isabelle -u Isabelle \
   -I "de.tum.in.isabelle" \
   -i "$THIS/../isabelle.icns" \
+  -D -X thy \
+  -Q "$THIS/../theory.icns" \
   -p /bin/bash \
-  -c "$THIS/script" \
+  -R \
   -o None \
   -f "$COCOADIALOG_APP" \
+  "$THIS/script" \
   "$PWD/Isabelle.app"
diff -r 2421ff8c57a5 -r 808a5ba61991 Admin/init_components
--- a/Admin/init_components	Mon Jul 23 18:52:10 2012 +0200
+++ b/Admin/init_components	Mon Jul 23 19:07:01 2012 +0200
@@ -5,22 +5,11 @@
 # init_components - bash source script to initialize components
 # as specified in the Admin directory
 
-function init_component_liberal
-{
-  local LOCATION="$1"
-  if [[ -d "${LOCATION}" ]]
-  then
-    init_component "${LOCATION}"
-  else
-    echo "Warning: no component found in ${LOCATION}" >&2
-  fi
-}
-
-while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
+while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
 do
-  case "${REPLY}" in
+  case "$REPLY" in
     \#* | "") ;;
-    /*) init_component_liberal "${REPLY}" ;;
-    *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
+    /*) init_component "$REPLY" ;;
+    *) init_component "$COMPONENT/$REPLY" ;;
   esac
-done < "${ISABELLE_HOME}/Admin/components"
+done < "$ISABELLE_HOME/Admin/components"
diff -r 2421ff8c57a5 -r 808a5ba61991 Admin/isatest/annomaly
--- a/Admin/isatest/annomaly	Mon Jul 23 18:52:10 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-#!/bin/sh
-
-# Create AnnoMaLy documentation for Isabelle
-# See http://martin.von-gagern.net/projects/annomaly/
-#   2007  Martin von Gagern (martin@von-gagern.net)
-
-# Abort on any error
-set -e -o pipefail
-
-BUILD_DIR="$HOME/isabelle.annomaly"
-ISABELLE_HOME="$BUILD_DIR/Isabelle"
-ISABELLE_CVS="$HOME/isabelle.cvs"
-ADMIN_CVS="$ISABELLE_CVS/Admin"
-# ISABELLE_HOME="$ISABELLE_CVS/Distribution"
-ISABELLE_SRC="$ISABELLE_HOME/src"
-HTML_DIR="$HOME/html-data/isabelle-doc"
-export CVS_RSH=ssh
-export SMLNJ_HOME="$HOME/annomaly"
-export PATH="$SMLNJ_HOME/bin:$PATH"
-export SML_DOC_DIR="$HTML_DIR.tmp"
-# export SML_DOC_DEBUG="all"
-TARGET=HOL
-CVSUP=true
-
-# Parse command line
-for ARG in "$@"; do case "$ARG" in
-	-p) TARGET=Pure ;;
-	-n) CVSUP=false ;;
-	-l) export SML_LOG_DIR="$HOME/logs" ;;
-esac; done
-
-# Update CVS
-cd "$ADMIN_CVS"
-if $CVSUP; then
-  echo "Updating CVS"
-  cvs -q up -d
-fi
-
-# Find nightly isabelle tarball
-ISABELLE_TAR=""
-for i in /home/html/isatest/Isabelle_[0-9]*-20[0-9][0-9].tar.gz; do
-  if [[ -r "$i" ]]; then ISABELLE_TAR="$i"; fi
-done
-if [[ -z $ISABELLE_TAR ]]; then
-  echo "No isabelle tarball found!" >&2
-  exit 1
-fi
-
-# Create build environemnt
-mkdir -p "$BUILD_DIR"
-cd "$BUILD_DIR"
-if [[ -d Isabelle ]]; then
-  rm -rf *
-fi
-tar xzf "$ISABELLE_TAR"
-cd "$ISABELLE_HOME"
-cp "$ADMIN_CVS"/isatest/annomaly.ML src/Pure/ML-Systems/annomaly.ML
-ln -s run-smlnj lib/scripts/run-annomaly
-
-# Create clean output directory
-rm -rf "$SML_DOC_DIR"
-mkdir "$SML_DOC_DIR"
-cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
-cat > "$SML_DOC_DIR/.htaccess" <<EOF
-DirectoryIndex index.html source.html
-<IfModule mod_deflate>
-SetOutputFilter DEFLATE 
-</IfModule>
-AddType text/plain .dot
-EOF
-
-# Build isabelle
-ISABELLE_HOME="$(cd "$ISABELLE_HOME"; pwd -P)"
-cd "$ISABELLE_HOME"
-export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
-rm -rf heaps
-./build -b $TARGET
-cd "$BUILD_DIR"
-rm -rf *
-
-# Postprocess created files
-cd $SML_DOC_DIR
-dot -Tsvg depGraph.dot \
-  | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
-  > depGraph.svg
-dot -Tps2 depGraph.dot > depGraph.ps
-ps2pdf depGraph.ps depGraph.pdf
-grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
-
-# Install result by renaming, to be almost atomic
-rm -rf "$HTML_DIR.bac"
-if [[ -d $HTML_DIR ]]; then mv "$HTML_DIR" "$HTML_DIR.bac"; fi
-mv "$SML_DOC_DIR" "$HTML_DIR"
-rm -rf "$HTML_DIR.bac"
-
-# Done
-echo "Completed successfully"
-exit 0
diff -r 2421ff8c57a5 -r 808a5ba61991 Admin/isatest/annomaly.ML
--- a/Admin/isatest/annomaly.ML	Mon Jul 23 18:52:10 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*  Title:      Admin/isatest/annomaly.ML
-    Author:     Martin von Gagern <martin@von-gagern.net>
-*)
-
-use "ML-Systems/smlnj.ML";
-
-local
-
-  val smlnj_use_text = use_text
-
-  val smlnj_use_file = use_file
-
-  val smlnj_forget_structure = forget_structure
-
-  fun mkAbsolute path =
-      OS.Path.mkAbsolute { path = path, relativeTo = OS.FileSys.getDir () }
-
-  fun toArcs path = #arcs (OS.Path.fromString path)
-
-  val isabelleHome =
-      case OS.Process.getEnv "ISABELLE_HOME"
-       of  NONE => OS.FileSys.getDir ()
-         | SOME home => mkAbsolute home
-
-  fun noparent [] = []
-    | noparent (n :: ns) =
-      if n = OS.Path.parentArc then noparent ns else n :: noparent ns
-
-  fun isabellePath [] = []
-    | isabellePath ("src" :: name) = "Isabelle" :: name
-    | isabellePath (name as (n :: ns)) =
-      if n = OS.Path.parentArc then noparent ns else "Isabelle" :: name
-
-  fun rewrite defPrefix name =
-      let val abs = mkAbsolute name
-          val rel = OS.Path.mkRelative { path = abs, relativeTo = isabelleHome }
-          val exists = (OS.FileSys.access(abs, nil)
-                        handle OS.SysErr _ => false)
-      in  if exists andalso rel <> ""
-          then isabellePath (toArcs rel)
-          else defPrefix @ noparent (toArcs name)
-      end handle OS.Path.Path => defPrefix @ noparent (toArcs name)
-
-in
-
-  fun use_text tune str_of_pos name_space (line, name) p v t =
-    let val name = case name of "" => "unnamed" | name => name
-        val arcs = rewrite ["use_text"] name
-        (* should we have different files for different line numbers? *
-        val arcs = if line <= 1 then arcs
-                   else arcs @ [ "l." ^ Int.toString line ]
-        *)
-        val arcs = if t = "structure Isabelle =\nstruct\nend;"
-                      andalso name = "ML"
-                   then ["empty_Isabelle", "empty" ] else arcs
-        val _    = AnnoMaLy.nameNextStream arcs
-    in  smlnj_use_text tune str_of_pos name_space (line, name) p v t  end;
-
-  fun use_file tune str_of_pos name_space output verbose name =
-      let val arcs = rewrite ["use_file"] name
-          val _    = AnnoMaLy.nameNextStream arcs
-      in  smlnj_use_file tune str_of_pos name_space output verbose name  end;
-
-  fun forget_structure name =
-      let val arcs = [ "forget_structure", name ]
-          val _    = AnnoMaLy.nameNextStream arcs
-      in  smlnj_forget_structure name  end;
-
-end;
diff -r 2421ff8c57a5 -r 808a5ba61991 Admin/isatest/isatest-annomaly
--- a/Admin/isatest/isatest-annomaly	Mon Jul 23 18:52:10 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-#!/usr/bin/env bash
-#
-# Create AnnoMaLy documentation for Isabelle
-#
-# Based on http://martin.von-gagern.net/projects/annomaly/
-#   2007  Martin von Gagern (martin@von-gagern.net)
-
-## global settings
-. ~/admin/isatest/isatest-settings
-
-PRG="$(basename "$0")"
-
-export SMLNJ_HOME="/home/gagern/annomaly"
-export SML_DOC_DIR="$HOME/anno-html"
-
-ADMIN="$HOME/admin/isatest"
-LOGICS="HOL"
-
-# Abort on any error
-set -e -o pipefail
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG"
-  echo
-  echo "  Generate html documentation from .ML files"
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  log "FAILED, $1"
-  exit 2
-}
-
-
-## main
-
-ISABELLE_HOME="$DISTPREFIX/Isabelle"
-ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
-
-[ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
-
-
-# Create clean output directory
-rm -rf "$SML_DOC_DIR"
-mkdir "$SML_DOC_DIR"
-cp "$SMLNJ_HOME/annomaly/resources/"* "$SML_DOC_DIR"
-cat > "$SML_DOC_DIR/.htaccess" <<EOF
-DirectoryIndex index.html source.html
-<IfModule mod_deflate>
-SetOutputFilter DEFLATE 
-</IfModule>
-AddType text/plain .dot
-EOF
-
-# Prepare build environemnt
-cd "$ISABELLE_HOME"
-cp "$ADMIN/annomaly.ML" src/Pure/ML-Systems/annomaly.ML
-ln -fs run-smlnj lib/scripts/run-annomaly
-
-cd "$ISABELLE_HOME"
-export SML_DOC_REWRITE="isabelle=$(cd src; pwd -P)"
-
-
-# Process image(s)
-for L in $LOGICS
-do
-  ( cd "$ISABELLE_HOME/src/$L"; \
-    cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
-    "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
-done
-
-
-# Postprocess created files
-cd "$SML_DOC_DIR"
-dot -Tsvg depGraph.dot \
-  | perl -pe 's/(width|height)="(\d+)/sprintf("%s=\"%.2f",$1,$2*0.6)/ge' \
-  > depGraph.svg
-dot -Tps2 depGraph.dot > depGraph.ps
-ps2pdf depGraph.ps depGraph.pdf
-
-# $ISABELLE_HOME does not seem to occur anywhere ??
-# grep -rl "$ISABELLE_HOME" . | xargs sed -i "s@$ISABELLE_HOME@\$ISABELLE_HOME@g"
-
-
-log "annomaly docs generated successfully."
diff -r 2421ff8c57a5 -r 808a5ba61991 Admin/isatest/settings/annomaly
--- a/Admin/isatest/settings/annomaly	Mon Jul 23 18:52:10 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-ML_SYSTEM=annomaly
-ML_HOME="$SMLNJ_HOME/bin"
-ML_OPTIONS="-m $SMLNJ_HOME/annomaly/annomaly.cm @SMLdebug=/dev/null"
-ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-
-
-ISABELLE_HOME_USER="$HOME/isabelle-annomaly"
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-
diff -r 2421ff8c57a5 -r 808a5ba61991 Admin/mira.py
--- a/Admin/mira.py	Mon Jul 23 18:52:10 2012 +0200
+++ b/Admin/mira.py	Mon Jul 23 19:07:01 2012 +0200
@@ -492,8 +492,8 @@
 
 smlnj_settings = '''
 ML_SYSTEM=smlnj
-ML_HOME="/home/smlnj/110.72/bin"
-ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
+ML_HOME="/home/smlnj/110.74/bin"
+ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
 '''
 
diff -r 2421ff8c57a5 -r 808a5ba61991 etc/settings
--- a/etc/settings	Mon Jul 23 18:52:10 2012 +0200
+++ b/etc/settings	Mon Jul 23 19:07:01 2012 +0200
@@ -45,7 +45,7 @@
 # Standard ML of New Jersey (slow!)
 #ML_SYSTEM=smlnj-110
 #ML_HOME="/usr/local/smlnj/bin"
-#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
+#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
 #SMLNJ_CYGWIN_RUNTIME=1
 
@@ -93,7 +93,11 @@
 ###
 
 # The place for user configuration, heap files, etc.
-ISABELLE_HOME_USER="$USER_HOME/.isabelle/${ISABELLE_IDENTIFIER:-.}"
+if [ -z "ISABELLE_IDENTIFIER" ]; then
+  ISABELLE_HOME_USER="$USER_HOME/.isabelle"
+else
+  ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
+fi
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
diff -r 2421ff8c57a5 -r 808a5ba61991 lib/Tools/build
--- a/lib/Tools/build	Mon Jul 23 18:52:10 2012 +0200
+++ b/lib/Tools/build	Mon Jul 23 19:07:01 2012 +0200
@@ -21,6 +21,7 @@
   echo "    -j INT       maximum number of jobs (default 1)"
   echo "    -l           list sessions only"
   echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
+  echo "    -s           system build mode: produce output in ISABELLE_HOME"
   echo "    -v           verbose"
   echo
   echo "  Build and manage Isabelle sessions, depending on implicit"
@@ -52,12 +53,13 @@
 BUILD_IMAGES=false
 MAX_JOBS=1
 LIST_ONLY=false
+SYSTEM_MODE=false
 VERBOSE=false
 
 declare -a MORE_DIRS=()
 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
 
-while getopts "abd:j:lo:v" OPT
+while getopts "abd:j:lo:sv" OPT
 do
   case "$OPT" in
     a)
@@ -79,6 +81,9 @@
     o)
       BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
       ;;
+    s)
+      SYSTEM_MODE="true"
+      ;;
     v)
       VERBOSE="true"
       ;;
@@ -96,5 +101,5 @@
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
 exec "$ISABELLE_TOOL" java isabelle.Build \
-  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$VERBOSE" \
+  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$VERBOSE" \
   "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
diff -r 2421ff8c57a5 -r 808a5ba61991 lib/Tools/usedir
--- a/lib/Tools/usedir	Mon Jul 23 18:52:10 2012 +0200
+++ b/lib/Tools/usedir	Mon Jul 23 19:07:01 2012 +0200
@@ -241,7 +241,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
+    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
     -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
@@ -250,7 +250,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
+    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
     -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
diff -r 2421ff8c57a5 -r 808a5ba61991 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Mon Jul 23 18:52:10 2012 +0200
+++ b/lib/scripts/getsettings	Mon Jul 23 19:07:01 2012 +0200
@@ -163,8 +163,7 @@
   esac
 
   if [ ! -d "$COMPONENT" ]; then
-    echo >&2 "Missing Isabelle component directory: \"$COMPONENT\""
-    exit 2
+    echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
   elif [ -z "$ISABELLE_COMPONENTS" ]; then
     ISABELLE_COMPONENTS="$COMPONENT"
   else
diff -r 2421ff8c57a5 -r 808a5ba61991 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Mon Jul 23 19:07:01 2012 +0200
@@ -11,7 +11,7 @@
 
 sledgehammer_params
   [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
-   lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
+   lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize]
 
 ML {*
 open MaSh_Export
@@ -66,5 +66,4 @@
   ()
 *}
 
-
 end
diff -r 2421ff8c57a5 -r 808a5ba61991 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -113,10 +113,6 @@
     handle TYPE _ => @{prop True}
   end
 
-fun all_non_tautological_facts_of thy css_table =
-  Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
-  |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd)
-
 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
   let
     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
@@ -126,7 +122,8 @@
     val mono = not (is_type_enc_polymorphic type_enc)
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val facts = all_non_tautological_facts_of thy css_table
+    val facts =
+      Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table
     val atp_problem =
       facts
       |> map (fn ((_, loc), th) =>
diff -r 2421ff8c57a5 -r 808a5ba61991 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -26,9 +26,7 @@
 
 val max_facts_slack = 2
 
-val all_names =
-  filter_out is_likely_tautology_or_too_meta
-  #> map (rpair () o nickname_of) #> Symtab.make
+val all_names = map (rpair () o nickname_of) #> Symtab.make
 
 fun evaluate_mash_suggestions ctxt params thy file_name =
   let
diff -r 2421ff8c57a5 -r 808a5ba61991 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -49,9 +49,7 @@
 val thy_name_of_fact = hd o Long_Name.explode
 fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
 
-val all_names =
-  filter_out is_likely_tautology_or_too_meta
-  #> map (rpair () o nickname_of) #> Symtab.make
+val all_names = map (rpair () o nickname_of) #> Symtab.make
 
 fun generate_accessibility thy include_thy file_name =
   let
diff -r 2421ff8c57a5 -r 808a5ba61991 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -88,11 +88,13 @@
   val isabelle_info : string -> int -> (string, 'a) ho_term list
   val extract_isabelle_status : (string, 'a) ho_term list -> string option
   val extract_isabelle_rank : (string, 'a) ho_term list -> int
+  val inductionN : string
   val introN : string
   val inductiveN : string
   val elimN : string
   val simpN : string
-  val defN : string
+  val non_rec_defN : string
+  val rec_defN : string
   val rankN : string
   val minimum_rank : int
   val default_rank : int
@@ -222,11 +224,14 @@
 
 val isabelle_info_prefix = "isabelle_"
 
+val inductionN = "induction"
 val introN = "intro"
 val inductiveN = "inductive"
 val elimN = "elim"
 val simpN = "simp"
-val defN = "def"
+val non_rec_defN = "non_rec_def"
+val rec_defN = "rec_def"
+
 val rankN = "rank"
 
 val minimum_rank = 0
@@ -503,9 +508,13 @@
     fun suffix_tag top_level s =
       if top_level then
         case extract_isabelle_status info of
-          SOME s' => if s' = defN then s ^ ":lt"
-                     else if s' = simpN andalso gen_simp then s ^ ":lr"
-                     else s
+          SOME s' =>
+          if s' = non_rec_defN then
+            s ^ ":lt"
+          else if (s' = simpN orelse s' = rec_defN) andalso gen_simp then
+            s ^ ":lr"
+          else
+            s
         | NONE => s
       else
         s
diff -r 2421ff8c57a5 -r 808a5ba61991 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -18,7 +18,9 @@
   datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
 
   datatype scope = Global | Local | Assum | Chained
-  datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
+  datatype status =
+    General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def |
+    Rec_Def
   type stature = scope * status
 
   datatype strictness = Strict | Non_Strict
@@ -103,6 +105,7 @@
   val helper_table : ((string * bool) * (status * thm) list) list
   val trans_lams_from_string :
     Proof.context -> type_enc -> string -> term list -> term list * term list
+  val string_of_status : status -> string
   val factsN : string
   val prepare_atp_problem :
     Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string
@@ -123,7 +126,8 @@
 datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
 
 datatype scope = Global | Local | Assum | Chained
-datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
+datatype status =
+  General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
 type stature = scope * status
 
 datatype order =
@@ -1236,7 +1240,8 @@
             |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
     val lam_facts =
       map2 (fn t => fn j =>
-               ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t)))
+               ((lam_fact_prefix ^ Int.toString j,
+                 (Global, Non_Rec_Def)), (Axiom, t)))
            lambda_ts (1 upto length lambda_ts)
   in (facts, lam_facts) end
 
@@ -1293,7 +1298,7 @@
               ((name, stature as (_, status)), t) =
   let
     val role =
-      if is_format_with_defs format andalso status = Def andalso
+      if is_format_with_defs format andalso status = Non_Rec_Def andalso
          is_legitimate_tptp_def t then
         Definition
       else
@@ -1664,18 +1669,18 @@
 
 (* The Boolean indicates that a fairly sound type encoding is needed. *)
 val base_helper_table =
-  [(("COMBI", false), [(Def, @{thm Meson.COMBI_def})]),
-   (("COMBK", false), [(Def, @{thm Meson.COMBK_def})]),
-   (("COMBB", false), [(Def, @{thm Meson.COMBB_def})]),
-   (("COMBC", false), [(Def, @{thm Meson.COMBC_def})]),
-   (("COMBS", false), [(Def, @{thm Meson.COMBS_def})]),
+  [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]),
+   (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]),
+   (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]),
+   (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]),
+   (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]),
    ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
    (("fFalse", false), [(General, not_ffalse)]),
    (("fFalse", true), [(General, @{thm True_or_False})]),
    (("fTrue", false), [(General, ftrue)]),
    (("fTrue", true), [(General, @{thm True_or_False})]),
    (("If", true),
-    [(Def, @{thm if_True}), (Def, @{thm if_False}),
+    [(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}),
      (General, @{thm True_or_False})])]
 
 val helper_table =
@@ -1683,7 +1688,7 @@
   [(("fNot", false),
     @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
            fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
-    |> map (pair Def)),
+    |> map (pair Non_Rec_Def)),
    (("fconj", false),
     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
         by (unfold fconj_def) fast+}
@@ -1718,19 +1723,19 @@
    ((app_op_name, true),
     [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]),
    (("fconj", false),
-    @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Def)),
+    @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
    (("fdisj", false),
-    @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Def)),
+    @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
    (("fimplies", false),
     @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
-    |> map (pair Def)),
+    |> map (pair Non_Rec_Def)),
    (("fequal", false),
-    (@{thms fequal_table} |> map (pair Def)) @
+    (@{thms fequal_table} |> map (pair Non_Rec_Def)) @
     (@{thms fequal_laws} |> map (pair General))),
    (("fAll", false),
-    @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)),
+    @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def)),
    (("fEx", false),
-    @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
+    @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def))]
   |> map (apsnd (map (apsnd zero_var_indexes)))
 
 fun bound_tvars type_enc sorts Ts =
@@ -2104,28 +2109,29 @@
       | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
   in do_formula end
 
+fun string_of_status General = ""
+  | string_of_status Induction = inductionN
+  | string_of_status Intro = introN
+  | string_of_status Inductive = inductiveN
+  | string_of_status Elim = elimN
+  | string_of_status Simp = simpN
+  | string_of_status Non_Rec_Def = non_rec_defN
+  | string_of_status Rec_Def = rec_defN
+
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP explicitly forbids name clashes, and some of
    the remote provers might care. *)
 fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank
-                  (j, {name, stature, role, iformula, atomic_types}) =
-  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role,
-   iformula
-   |> formula_from_iformula ctxt mono type_enc should_guard_var_in_formula
-                            (if pos then SOME true else NONE)
-   |> close_formula_universally
-   |> bound_tvars type_enc true atomic_types,
-   NONE,
-   let val rank = rank j in
-     case snd stature of
-       Intro => isabelle_info introN rank
-     | Inductive => isabelle_info inductiveN rank
-     | Elim => isabelle_info elimN rank
-     | Simp => isabelle_info simpN rank
-     | Def => isabelle_info defN rank
-     | _ => isabelle_info "" rank
-   end)
-  |> Formula
+        (j, {name, stature = (_, status), role, iformula, atomic_types}) =
+  Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
+           encode name,
+           role,
+           iformula
+           |> formula_from_iformula ctxt mono type_enc
+                  should_guard_var_in_formula (if pos then SOME true else NONE)
+           |> close_formula_universally
+           |> bound_tvars type_enc true atomic_types,
+           NONE, isabelle_info (string_of_status status) (rank j))
 
 fun lines_for_subclass type_enc sub super =
   Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom,
@@ -2355,7 +2361,7 @@
              Axiom,
              eq_formula type_enc (atomic_types_of T) [] false
                   (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
-             NONE, isabelle_info defN helper_rank)
+             NONE, isabelle_info non_rec_defN helper_rank)
   end
 
 fun lines_for_mono_types ctxt mono type_enc Ts =
@@ -2438,7 +2444,7 @@
     val tag_with = tag_with_type ctxt mono type_enc NONE
     fun formula c =
       [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info
-                defN helper_rank)]
+                non_rec_defN helper_rank)]
   in
     if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
       []
@@ -2538,7 +2544,7 @@
       in
         ([tm1, tm2],
          [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate,
-                   NONE, isabelle_info defN helper_rank)])
+                   NONE, isabelle_info non_rec_defN helper_rank)])
         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
             else pair_append (do_alias (ary - 1)))
       end
@@ -2878,8 +2884,9 @@
     fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
     val graph =
       Graph.empty
-      |> fold (fold (add_eq_deps (has_status defN)) o snd) problem
-      |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem
+      |> fold (fold (add_eq_deps (has_status non_rec_defN)) o snd) problem
+      |> fold (fold (add_eq_deps (has_status rec_defN orf has_status simpN
+                                  orf is_conj)) o snd) problem
       |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem
       |> fold (fold (add_intro_deps (has_status introN)) o snd) problem
     fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
diff -r 2421ff8c57a5 -r 808a5ba61991 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -200,10 +200,11 @@
   else
     isa_ext
 
-fun add_all_defs fact_names accum =
+fun add_non_rec_defs fact_names accum =
   Vector.foldl
       (fn (facts, facts') =>
-          union (op =) (filter (fn (_, (_, status)) => status = Def) facts)
+          union (op =)
+                (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
                 facts')
       accum fact_names
 
@@ -214,12 +215,12 @@
        (* LEO 1.3.3 does not record definitions properly, leading to missing
          dependencies in the TSTP proof. Remove the next line once this is
          fixed. *)
-       add_all_defs fact_names
+       add_non_rec_defs fact_names
      else if rule = satallax_unsat_coreN then
        (fn [] =>
            (* Satallax doesn't include definitions in its unsatisfiable cores,
               so we assume the worst and include them all here. *)
-           [(ext_name ctxt, (Global, General))] |> add_all_defs fact_names
+           [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
          | facts => facts)
      else
        I)
diff -r 2421ff8c57a5 -r 808a5ba61991 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -23,7 +23,6 @@
   val fact_from_ref :
     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
-  val is_likely_tautology_or_too_meta : thm -> bool
   val backquote_thm : thm -> string
   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
   val maybe_instantiate_inducts :
@@ -50,8 +49,6 @@
    del : (Facts.ref * Attrib.src list) list,
    only : bool}
 
-val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-
 (* experimental features *)
 val ignore_no_atp =
   Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
@@ -147,10 +144,11 @@
 fun multi_base_blacklist ctxt ho_atp =
   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
    "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
-   "weak_case_cong"]
+   "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
+   "nibble.distinct"]
   |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
         append ["induct", "inducts"]
-  |> map (prefix ".")
+  |> map (prefix Long_Name.separator)
 
 val max_lambda_nesting = 3 (*only applies if not ho_atp*)
 
@@ -162,12 +160,11 @@
 
 (* Don't count nested lambdas at the level of formulas, since they are
    quantifiers. *)
-fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*)
-  | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) =
-      formula_has_too_many_lambdas false (T :: Ts) t
-  | formula_has_too_many_lambdas _ Ts t =
+fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
+    formula_has_too_many_lambdas (T :: Ts) t
+  | formula_has_too_many_lambdas Ts t =
     if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
-      exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t))
+      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
     else
       term_has_too_many_lambdas max_lambda_nesting t
 
@@ -180,11 +177,17 @@
   | apply_depth _ = 0
 
 fun is_formula_too_complex ho_atp t =
-  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t
+  apply_depth t > max_apply_depth orelse
+  (not ho_atp andalso formula_has_too_many_lambdas [] t)
 
-(* FIXME: Extend to "Meson" and "Metis" *)
+(* These theories contain auxiliary facts that could positively confuse
+   Sledgehammer if they were included. *)
+val sledgehammer_prefixes =
+  ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator)
+
 val exists_sledgehammer_const =
-  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
+  exists_Const (fn (s, _) =>
+      exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes)
 
 (* FIXME: make more reliable *)
 val exists_low_level_class_const =
@@ -192,25 +195,11 @@
      s = @{const_name equal_class.equal} orelse
      String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
 
-fun is_metastrange_theorem th =
-  case head_of (concl_of th) of
-    Const (s, _) => (s <> @{const_name Trueprop} andalso
-                     s <> @{const_name "=="})
-  | _ => false
-
 fun is_that_fact th =
   String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
   andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
                            | _ => false) (prop_of th)
 
-fun is_theorem_bad_for_atps ho_atp thm =
-  is_metastrange_theorem thm orelse
-  let val t = prop_of thm in
-    is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse
-    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
-    is_that_fact thm
-  end
-
 fun is_likely_tautology_or_too_meta th =
   let
     val is_boring_const = member (op =) atp_widely_irrelevant_consts
@@ -229,6 +218,15 @@
     is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
   end
 
+fun is_theorem_bad_for_atps ho_atp th =
+  is_likely_tautology_or_too_meta th orelse
+  let val t = prop_of th in
+    is_formula_too_complex ho_atp t orelse
+    exists_type type_has_top_sort t orelse
+    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
+    is_that_fact th
+  end
+
 fun hackish_string_for_term thy t =
   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                    (print_mode_value ())) (Syntax.string_of_term_global thy) t
@@ -299,8 +297,8 @@
             |> maps (snd o snd)
   in
     Termtab.empty |> add Simp [atomize] snd simps
-                  |> add Simp [] I rec_defs
-                  |> add Def [] I nonrec_defs
+                  |> add Rec_Def [] I rec_defs
+                  |> add Non_Rec_Def [] I nonrec_defs
 (* Add once it is used:
                   |> add Elim [] I elims
 *)
@@ -458,7 +456,6 @@
        else
          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
            all_facts ctxt ho_atp reserved add chained css
-           |> filter_out (is_likely_tautology_or_too_meta o snd)
            |> filter_out (member Thm.eq_thm_prop del o snd)
            |> maybe_filter_no_atps ctxt
            |> uniquify
diff -r 2421ff8c57a5 -r 808a5ba61991 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -29,7 +29,7 @@
 open Sledgehammer_MaSh
 open Sledgehammer_Run
 
-val cvc3N = "cvc3"
+(* val cvc3N = "cvc3" *)
 val yicesN = "yices"
 val z3N = "z3"
 
@@ -226,7 +226,7 @@
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put E first. *)
 fun default_provers_param_value ctxt =
-  [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN, cvc3N]
+  [eN, spassN, vampireN, z3N, e_sineN, waldmeisterN, yicesN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
                                   max_default_remote_threads)
@@ -404,11 +404,11 @@
        else
          ();
        mash_learn ctxt (get_params Normal ctxt
-                           (("timeout",
-                             [string_of_real default_learn_atp_timeout]) ::
+                           ([("timeout",
+                              [string_of_real default_learn_atp_timeout]),
+                             ("slice", ["false"])] @
                             override_params @
-                            [("slice", ["false"]),
-                             ("minimize", ["true"]),
+                            [("minimize", ["true"]),
                              ("preplay_timeout", ["0"])]))
                   fact_override (#facts (Proof.goal state))
                   (subcommand = learn_atpN orelse subcommand = relearn_atpN))
diff -r 2421ff8c57a5 -r 808a5ba61991 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -59,7 +59,7 @@
   val mash_can_suggest_facts : Proof.context -> bool
   val mash_suggested_facts :
     Proof.context -> params -> string -> int -> term list -> term
-    -> ('a * thm) list -> (('a * thm) * real) list * ('a * thm) list
+    -> fact list -> (fact * real) list * fact list
   val mash_learn_proof :
     Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
     -> unit
@@ -106,7 +106,7 @@
   getenv "ISABELLE_HOME_USER" ^ "/mash"
   |> tap (Isabelle_System.mkdir o Path.explode)
 val mash_state_dir = mash_model_dir
-fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
+fun mash_state_file () = mash_state_dir () ^ "/state"
 
 
 (*** Isabelle helpers ***)
@@ -312,25 +312,44 @@
   |> forall is_lambda_free ts ? cons "no_lams"
   |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
   |> scope <> Global ? cons "local"
-  |> (case status of
-        General => I
-      | Induction => cons "induction"
-      | Intro => cons "intro"
-      | Inductive => cons "inductive"
-      | Elim => cons "elim"
-      | Simp => cons "simp"
-      | Def => cons "def")
+  |> (case string_of_status status of "" => I | s => cons s)
 
 (* Too many dependencies is a sign that a decision procedure is at work. There
    isn't much too learn from such proofs. *)
-val max_dependencies = 10
+val max_dependencies = 20
 val atp_dependency_default_max_fact = 50
 
-fun trim_dependencies deps =
-  if length deps <= max_dependencies then SOME deps else NONE
+(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
+val typedef_deps = [@{thm CollectI} |> nickname_of]
+
+(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
+val typedef_ths =
+  @{thms type_definition.Abs_inverse type_definition.Rep_inverse
+         type_definition.Rep type_definition.Rep_inject
+         type_definition.Abs_inject type_definition.Rep_cases
+         type_definition.Abs_cases type_definition.Rep_induct
+         type_definition.Abs_induct type_definition.Rep_range
+         type_definition.Abs_image}
+  |> map nickname_of
 
-fun isar_dependencies_of all_names =
-  thms_in_proof (SOME all_names) #> trim_dependencies
+fun is_size_def [dep] th =
+    (case first_field ".recs" dep of
+       SOME (pref, _) =>
+       (case first_field ".size" (nickname_of th) of
+          SOME (pref', _) => pref = pref'
+        | NONE => false)
+     | NONE => false)
+  | is_size_def _ _ = false
+
+fun trim_dependencies th deps =
+  if length deps > max_dependencies orelse deps = typedef_deps orelse
+     exists (member (op =) typedef_ths) deps orelse is_size_def deps th then
+    NONE
+  else
+    SOME deps
+
+fun isar_dependencies_of all_names th =
+  th |> thms_in_proof (SOME all_names) |> trim_dependencies th
 
 fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
                         auto_level facts all_names th =
@@ -376,7 +395,7 @@
            end
          else
            ();
-         used_facts |> map fst |> trim_dependencies)
+         used_facts |> map fst |> trim_dependencies th)
       | _ => NONE
     end
 
@@ -385,11 +404,11 @@
 
 (* more friendly than "try o File.rm" for those who keep the files open in their
    text editor *)
-fun wipe_out file = File.write file ""
+fun wipe_out_file file = File.write (Path.explode file) ""
 
-fun write_file (xs, f) file =
+fun write_file heading (xs, f) file =
   let val path = Path.explode file in
-    wipe_out path;
+    File.write path heading;
     xs |> chunk_list 500
        |> List.app (File.append path o space_implode "" o map f)
   end
@@ -411,8 +430,8 @@
       mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
       " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
   in
-    write_file ([], K "") sugg_file;
-    write_file write_cmds cmd_file;
+    write_file "" ([], K "") sugg_file;
+    write_file "" write_cmds cmd_file;
     trace_msg ctxt (fn () => "Running " ^ command);
     Isabelle_System.bash command;
     read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
@@ -422,8 +441,7 @@
            | SOME "" => "Done"
            | SOME s => "Error: " ^ elide_string 1000 s))
     |> not overlord
-       ? tap (fn _ => List.app (wipe_out o Path.explode)
-                               [err_file, sugg_file, cmd_file])
+       ? tap (fn _ => List.app wipe_out_file [err_file, sugg_file, cmd_file])
   end
 
 fun str_of_add (name, parents, feats, deps) =
@@ -506,7 +524,7 @@
 
 fun load _ (state as (true, _)) = state
   | load ctxt _ =
-    let val path = mash_state_path () in
+    let val path = mash_state_file () |> Path.explode in
       (true,
        case try File.read_lines path of
          SOME (version' :: node_lines) =>
@@ -531,15 +549,13 @@
 
 fun save ctxt {fact_G} =
   let
-    val path = mash_state_path ()
-    fun fact_line_for name parents =
-      escape_meta name ^ ": " ^ escape_metas parents
-    val append_fact = File.append path o suffix "\n" oo fact_line_for
-    fun append_entry (name, ((), (parents, _))) () =
-      append_fact name (Graph.Keys.dest parents)
+    fun str_of_entry (name, parents) =
+      escape_meta name ^ ": " ^ escape_metas parents ^ "\n"
+    fun append_entry (name, ((), (parents, _))) =
+      cons (name, Graph.Keys.dest parents)
+    val entries = [] |> Graph.fold append_entry fact_G
   in
-    File.write path (version ^ "\n");
-    Graph.fold append_entry fact_G ();
+    write_file (version ^ "\n") (entries, str_of_entry) (mash_state_file ());
     trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")")
   end
 
@@ -551,12 +567,17 @@
 fun mash_map ctxt f =
   Synchronized.change global_state (load ctxt ##> (f #> tap (save ctxt)))
 
+fun mash_peek ctxt f =
+  Synchronized.change_result global_state (load ctxt #> `snd #>> f)
+
 fun mash_get ctxt =
   Synchronized.change_result global_state (load ctxt #> `snd)
 
 fun mash_unlearn ctxt =
   Synchronized.change global_state (fn _ =>
-      (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state)))
+      (mash_CLEAR ctxt;
+       wipe_out_file (mash_state_file ());
+       (true, empty_state)))
 
 end
 
@@ -598,28 +619,43 @@
 (* Generate more suggestions than requested, because some might be thrown out
    later for various reasons and "meshing" gives better results with some
    slack. *)
-fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
+fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts)
 
 fun is_fact_in_graph fact_G (_, th) =
   can (Graph.get_node fact_G) (nickname_of th)
 
+fun interleave 0 _ _ = []
+  | interleave n [] ys = take n ys
+  | interleave n xs [] = take n xs
+  | interleave 1 (x :: _) _ = [x]
+  | interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys
+
 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                          concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
-    val fact_G = #fact_G (mash_get ctxt)
-    val parents = maximal_in_graph fact_G facts
-    val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
-    val suggs =
-      if Graph.is_empty fact_G then []
-      else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
-    val selected =
+    val (fact_G, suggs) =
+      mash_peek ctxt (fn {fact_G} =>
+          if Graph.is_empty fact_G then
+            (fact_G, [])
+          else
+            let
+              val parents = maximal_in_graph fact_G facts
+              val feats =
+                features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
+            in
+              (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts)
+                                  (parents, feats))
+            end)
+    val sels =
       facts |> suggested_facts suggs
             (* The weights currently returned by "mash.py" are too extreme to
                make any sense. *)
-            |> map fst |> weight_mepo_facts
-    val unknown = facts |> filter_out (is_fact_in_graph fact_G)
-  in (selected, unknown) end
+            |> map fst
+    val (unk_global, unk_local) =
+      facts |> filter_out (is_fact_in_graph fact_G)
+            |> List.partition (fn ((_, (scope, _)), _) => scope = Global)
+  in (interleave max_facts unk_local sels |> weight_mepo_facts, unk_global) end
 
 fun add_to_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
   let
@@ -638,7 +674,7 @@
     val hard_timeout = time_mult learn_timeout_slack timeout
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, hard_timeout)
-    val desc = ("machine learner for Sledgehammer", "")
+    val desc = ("Machine learner for Sledgehammer", "")
   in Async_Manager.launch MaShN birth_time death_time desc task end
 
 fun freshish_name () =
@@ -656,12 +692,22 @@
           val name = freshish_name ()
           val feats = features_of ctxt prover thy (Local, General) [t]
           val deps = used_ths |> map nickname_of
-          val {fact_G} = mash_get ctxt
-          val parents = maximal_in_graph fact_G facts
         in
-          mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "")
+          mash_peek ctxt (fn {fact_G} =>
+              let val parents = maximal_in_graph fact_G facts in
+                mash_ADD ctxt overlord [(name, parents, feats, deps)]
+              end);
+          (true, "")
         end)
 
+val evil_theories =
+  ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
+   "New_DSequence", "New_Random_Sequence", "Quickcheck",
+   "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
+
+fun fact_has_evil_theory (_, th) =
+  member (op =) evil_theories (Context.theory_name (theory_of_thm th))
+
 fun sendback sub =
   Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
 
@@ -676,7 +722,8 @@
       Time.+ (Timer.checkRealTimer timer, commit_timeout)
     val {fact_G} = mash_get ctxt
     val (old_facts, new_facts) =
-      facts |> List.partition (is_fact_in_graph fact_G)
+      facts |> filter_out fact_has_evil_theory
+            |> List.partition (is_fact_in_graph fact_G)
             ||> sort (thm_ord o pairself snd)
   in
     if null new_facts andalso (not atp orelse null old_facts) then
@@ -691,15 +738,14 @@
     else
       let
         val all_names =
-          facts |> map snd
-                |> filter_out is_likely_tautology_or_too_meta
-                |> map (rpair () o nickname_of)
-                |> Symtab.make
-        val deps_of =
-          if atp then
-            atp_dependencies_of ctxt params prover auto_level facts all_names
+          facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make
+        fun deps_of status th =
+          if status = Non_Rec_Def orelse status = Rec_Def then
+            SOME []
+          else if atp then
+            atp_dependencies_of ctxt params prover auto_level facts all_names th
           else
-            isar_dependencies_of all_names
+            isar_dependencies_of all_names th
         fun do_commit [] [] state = state
           | do_commit adds reps {fact_G} =
             let
@@ -727,13 +773,13 @@
            else
              ())
         fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
-          | learn_new_fact ((_, stature), th)
+          | learn_new_fact ((_, stature as (_, status)), th)
                            (adds, (parents, n, next_commit, _)) =
             let
               val name = nickname_of th
               val feats =
                 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
-              val deps = deps_of th |> these
+              val deps = deps_of status th |> these
               val n = n |> not (null deps) ? Integer.add 1
               val adds = (name, parents, feats, deps) :: adds
               val (adds, next_commit) =
@@ -759,11 +805,12 @@
                 |> fold learn_new_fact new_facts
             in commit true adds []; n end
         fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
-          | relearn_old_fact (_, th) (reps, (n, next_commit, _)) =
+          | relearn_old_fact ((_, (_, status)), th)
+                             (reps, (n, next_commit, _)) =
             let
               val name = nickname_of th
               val (n, reps) =
-                case deps_of th of
+                case deps_of status th of
                   SOME deps => (n + 1, (name, deps) :: reps)
                 | NONE => (n, reps)
               val (reps, next_commit) =
@@ -774,7 +821,7 @@
               val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
             in (reps, (n, next_commit, timed_out)) end
         val n =
-          if null old_facts then
+          if not atp orelse null old_facts then
             n
           else
             let
diff -r 2421ff8c57a5 -r 808a5ba61991 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/Pure/General/file.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -45,11 +45,7 @@
 
 val platform_path = Path.implode o Path.expand;
 
-fun shell_quote s =
-  if exists_string (fn c => c = "'") s then
-    error ("Illegal single quote in path specification: " ^ quote s)
-  else enclose "'" "'" s;
-
+val shell_quote = enclose "'" "'";
 val shell_path = shell_quote o platform_path;
 
 
diff -r 2421ff8c57a5 -r 808a5ba61991 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/Pure/System/build.scala	Mon Jul 23 19:07:01 2012 +0200
@@ -340,20 +340,20 @@
     def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
   }
 
-  private def start_job(save: Boolean, name: String, info: Session.Info): Job =
+  private def start_job(name: String, info: Session.Info, output: Option[String]): Job =
   {
     val parent = info.parent.getOrElse("")
 
     val cwd = info.dir.file
-    val env = Map("INPUT" -> parent, "TARGET" -> name)
+    val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse(""))
     val script =
-      if (is_pure(name)) "./build " + (if (save) "-b " else "") + name
+      if (is_pure(name)) "./build " + name + " \"$OUTPUT\""
       else {
         """
         . "$ISABELLE_HOME/lib/scripts/timestart.bash"
         """ +
-          (if (save)
-            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
+          (if (output.isDefined)
+            """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """
           else
             """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
         """
@@ -372,7 +372,7 @@
     {
       import XML.Encode._
       pair(bool, pair(string, pair(string, list(string))))(
-        save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
+        output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
     }
     new Job(cwd, env, script, YXML.string_of_body(args_xml))
   }
@@ -384,29 +384,31 @@
   private def sleep(): Unit = Thread.sleep(500)
 
   def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
-    list_only: Boolean, verbose: Boolean,
+    list_only: Boolean, system_mode: Boolean, verbose: Boolean,
     more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
   {
     val options = (Options.init() /: more_options)(_.define_simple(_))
     val queue = find_sessions(options, all_sessions, sessions, more_dirs)
     val deps = dependencies(queue)
 
+    val (output_dir, browser_info) =
+      if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info"))
+      else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO"))
 
     // prepare browser info dir
-    if (options.bool("browser_info") &&
-      !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
+    if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
     {
-      Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
-      File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
-        Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
-      File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
-        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
-        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
-        File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
+      browser_info.file.mkdirs()
+      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
+        browser_info + Path.explode("isabelle.gif"))
+      File.write(browser_info + Path.explode("index.html"),
+        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
+        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
     }
 
     // prepare log dir
-    val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
+    val log_dir = output_dir + Path.explode("log")
     log_dir.file.mkdirs()
 
     // scheduler loop
@@ -447,9 +449,12 @@
               loop(pending - name, running, results + (name -> 0))
             }
             else if (info.parent.map(results(_)).forall(_ == 0)) {
-              val save = build_images || queue.is_inner(name)
-              echo((if (save) "Building " else "Running ") + name + " ...")
-              val job = start_job(save, name, info)
+              val output =
+                if (build_images || queue.is_inner(name))
+                  Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
+                else None
+              echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
+              val job = start_job(name, info, output)
               loop(pending, running + (name -> job), results)
             }
             else {
@@ -477,10 +482,11 @@
           Properties.Value.Boolean(build_images) ::
           Properties.Value.Int(max_jobs) ::
           Properties.Value.Boolean(list_only) ::
+          Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(verbose) ::
           Command_Line.Chunks(more_dirs, options, sessions) =>
-            build(all_sessions, build_images, max_jobs, list_only, verbose,
-              more_dirs.map(Path.explode), options, sessions)
+            build(all_sessions, build_images, max_jobs, list_only, system_mode,
+              verbose, more_dirs.map(Path.explode), options, sessions)
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }
diff -r 2421ff8c57a5 -r 808a5ba61991 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/Pure/System/session.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -10,7 +10,7 @@
   val name: unit -> string
   val welcome: unit -> string
   val init: bool -> string -> string -> unit
-  val use_dir: string -> string -> bool -> string list -> bool -> bool ->
+  val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     string -> bool -> string list -> string -> string -> bool * string ->
     string -> int -> bool -> bool -> int -> int -> int -> int -> unit
   val finish: unit -> unit
@@ -94,12 +94,12 @@
 fun dumping (_, "") = NONE
   | dumping (cp, path) = SOME (cp, Path.explode path);
 
-fun use_dir item root build modes reset info doc doc_graph doc_variants parent
+fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
      (init reset parent name;
-      Present.init build info doc doc_graph doc_variants (path ()) name
+      Present.init build info info_path doc doc_graph doc_variants (path ()) name
         (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
       if timing then
         let
diff -r 2421ff8c57a5 -r 808a5ba61991 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/Pure/Thy/present.ML	Mon Jul 23 19:07:01 2012 +0200
@@ -17,7 +17,7 @@
    path: string, parents: string list} list -> Path.T -> unit
   val display_graph: {name: string, ID: string, dir: string, unfold: bool,
    path: string, parents: string list} list -> unit
-  val init: bool -> bool -> string -> bool -> string list -> string list ->
+  val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
     string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
     theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
@@ -34,8 +34,6 @@
 
 (** paths **)
 
-val output_path = Path.variable "ISABELLE_BROWSER_INFO";
-
 val tex_ext = Path.ext "tex";
 val tex_path = tex_ext o Path.basic;
 val html_ext = Path.ext "html";
@@ -275,7 +273,7 @@
 
 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
 
-fun init build info doc doc_graph doc_variants path name dump_prefix
+fun init build info info_path doc doc_graph doc_variants path name dump_prefix
     (remote_path, first_time) verbose thys =
   if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
     (browser_info := empty_browser_info; session_info := NONE)
@@ -284,7 +282,7 @@
       val parent_name = name_of_session (take (length path - 1) path);
       val session_name = name_of_session path;
       val sess_prefix = Path.make path;
-      val html_prefix = Path.append (Path.expand output_path) sess_prefix;
+      val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
 
       val documents =
         if doc = "" then []
diff -r 2421ff8c57a5 -r 808a5ba61991 src/Pure/build
--- a/src/Pure/build	Mon Jul 23 18:52:10 2012 +0200
+++ b/src/Pure/build	Mon Jul 23 19:07:01 2012 +0200
@@ -12,12 +12,7 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG [OPTIONS] TARGET"
-  echo
-  echo "  Options are:"
-  echo "    -b           build target images"
-  echo
-  echo "  Build Isabelle/ML TARGET: RAW or Pure"
+  echo "Usage: $PRG TARGET OUTPUT"
   echo
   exit 1
 }
@@ -33,32 +28,14 @@
 
 ## process command line
 
-# options
-
-BUILD_IMAGES=false
-
-while getopts "b" OPT
-do
-  case "$OPT" in
-    b)
-      BUILD_IMAGES="true"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
 # args
 
-TARGET="Pure"
-[ "$#" -ge 1 ] && { TARGET="$1"; shift; }
-[ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\""
-
-[ "$#" -eq 0 ] || usage
+if [ "$#" -eq 2 ]; then
+  TARGET="$1"; shift
+  OUTPUT="$1"; shift
+else
+  usage
+fi
 
 
 ## main
@@ -79,7 +56,7 @@
 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
 if [ "$TARGET" = RAW ]; then
-  if [ "$BUILD_IMAGES" = false ]; then
+  if [ -z "$OUTPUT" ]; then
     "$ISABELLE_PROCESS" \
       -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
       -q RAW_ML_SYSTEM
@@ -88,10 +65,10 @@
       -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
       -e "structure Isar = struct fun main () = () end;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
-      -q -w RAW_ML_SYSTEM RAW
+      -q -w RAW_ML_SYSTEM "$OUTPUT"
   fi
 else
-  if [ "$BUILD_IMAGES" = false ]; then
+  if [ -z "$OUTPUT" ]; then
     "$ISABELLE_PROCESS" \
       -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
       -q RAW_ML_SYSTEM
@@ -99,7 +76,7 @@
     "$ISABELLE_PROCESS" \
       -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
       -e "ml_prompts \"ML> \" \"ML# \";" \
-      -f -q -w RAW_ML_SYSTEM Pure
+      -f -q -w RAW_ML_SYSTEM "$OUTPUT"
   fi
 fi