merged

--- a/Admin/isatest/isatest-makeall	Tue Jul 14 13:48:03 2015 +0200
+++ b/Admin/isatest/isatest-makeall	Tue Jul 14 19:08:40 2015 +0200
@@ -18,7 +18,7 @@
 function usage()
 {
   echo
-  echo "Usage: $PRG [-l targets] settings1 [settings2 ...]"
+  echo "Usage: $PRG [-x SESSION] [-l SESSIONS] settings1 [settings2 ...]"
   echo
   echo "  Runs isabelle build for specified settings."
   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
@@ -47,6 +47,7 @@
 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
 
 # build args and nice setup for different target platforms
+BUILD_OPTS=""
 BUILD_ARGS="-v"
 NICE="nice"
 case $HOSTNAME in
@@ -65,6 +66,13 @@
 
 ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
 
+if [ "$1" = "-x" ]; then
+  shift
+  [ "$#" -lt 2 ] && usage
+  BUILD_OPTS="$BUILD_OPTS -x $1"
+  shift
+fi
+
 if [ "$1" = "-l" ]; then
   shift
   [ "$#" -lt 2 ] && usage
@@ -122,7 +130,7 @@
 
     cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
-    (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_ARGS >> $TESTLOG 2>&1)
+    (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_OPTS -- $BUILD_ARGS >> $TESTLOG 2>&1)
 
     if [ $? -eq 0 ]
     then

--- a/Admin/isatest/isatest-makedist	Tue Jul 14 13:48:03 2015 +0200
+++ b/Admin/isatest/isatest-makedist	Tue Jul 14 19:08:40 2015 +0200
@@ -100,7 +100,7 @@
 
 ## spawn test runs
 
-$SSH lxbroy10 "$MAKEALL $HOME/settings/at64-poly"
+$SSH lxbroy10 "$MAKEALL -x HOL-Proofs $HOME/settings/at64-poly"
 sleep 15
 $SSH lxbroy4 "
   $MAKEALL -l HOL-Library $HOME/settings/at-poly;

--- a/Admin/isatest/settings/at64-poly	Tue Jul 14 13:48:03 2015 +0200
+++ b/Admin/isatest/settings/at64-poly	Tue Jul 14 19:08:40 2015 +0200
@@ -22,4 +22,4 @@
 ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
-ISABELLE_BUILD_OPTIONS="threads=1 -x HOL-Proofs"
+ISABELLE_BUILD_OPTIONS="threads=1"

--- a/src/Pure/Isar/proof.ML	Tue Jul 14 13:48:03 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jul 14 19:08:40 2015 +0200
@@ -498,7 +498,7 @@
     fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
 
     val th =
-      (Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal)
+      (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
         handle THM _ => err_lost ())
       |> Drule.flexflex_unique (SOME ctxt)
       |> Thm.check_shyps (Variable.sorts_of ctxt)

--- a/src/Pure/goal.ML	Tue Jul 14 13:48:03 2015 +0200
+++ b/src/Pure/goal.ML	Tue Jul 14 19:08:40 2015 +0200
@@ -230,7 +230,9 @@
             result)
           (Thm.term_of stmt);
   in
-    Conjunction.elim_balanced (length props) res
+    res
+    |> length props > 1 ? Thm.close_derivation
+    |> Conjunction.elim_balanced (length props)
     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt
     |> map Drule.zero_var_indexes