# HG changeset patch
# User wenzelm
# Date 1379352633 -7200
# Node ID cee071d331610a9ad6b1a6977e00e0b778c40ce1
# Parent  aeb3cf02c678e6a3c199c5ea1d8744894485c524# Parent  5ccee1cb245a8c6a014d3e20d19b3d74054467d1
merged

diff -r aeb3cf02c678 -r cee071d33161 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Mon Sep 16 16:48:08 2013 +0200
+++ b/Admin/Release/CHECKLIST	Mon Sep 16 19:30:33 2013 +0200
@@ -7,7 +7,9 @@
 
 - test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
 
-- test Proof General 4.1, 3.7.1.1;
+- test Isabelle/jEdit on single-core;
+
+- test Isabelle/jEdit on airy device;
 
 - test 'display_drafts' command;
 
@@ -17,6 +19,8 @@
 
 - check file positions within logic images (hyperlinks etc.);
 
+- check ML sources: isabelle build -nal;
+
 - run isabelle update_keywords;
 
 - check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
diff -r aeb3cf02c678 -r cee071d33161 Admin/Windows/Cygwin/Cygwin-Latex-Setup.bat
--- a/Admin/Windows/Cygwin/Cygwin-Latex-Setup.bat	Mon Sep 16 16:48:08 2013 +0200
+++ b/Admin/Windows/Cygwin/Cygwin-Latex-Setup.bat	Mon Sep 16 19:30:33 2013 +0200
@@ -1,4 +1,4 @@
 @echo off
 
-"%CD%\contrib\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2013 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin" --packages texlive-collection-latexextra,texlive-collection-fontutils,texlive-collection-mathextra,libsasl2 --quiet-mode
+"%CD%\contrib\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2013-1 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin" --packages texlive-collection-latexextra,texlive-collection-fontutils,texlive-collection-mathextra,libsasl2 --quiet-mode
 
diff -r aeb3cf02c678 -r cee071d33161 Admin/Windows/Cygwin/Cygwin-Setup.bat
--- a/Admin/Windows/Cygwin/Cygwin-Setup.bat	Mon Sep 16 16:48:08 2013 +0200
+++ b/Admin/Windows/Cygwin/Cygwin-Setup.bat	Mon Sep 16 19:30:33 2013 +0200
@@ -1,4 +1,4 @@
 @echo off
 
-"%CD%\contrib\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2013 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin"
+"%CD%\contrib\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2013-1 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin"
 
diff -r aeb3cf02c678 -r cee071d33161 Admin/Windows/Cygwin/README
--- a/Admin/Windows/Cygwin/README	Mon Sep 16 16:48:08 2013 +0200
+++ b/Admin/Windows/Cygwin/README	Mon Sep 16 19:30:33 2013 +0200
@@ -9,6 +9,7 @@
 * Local snapshots:
   http://isabelle.in.tum.de/cygwin  (Isabelle2012)
   http://isabelle.in.tum.de/cygwin_2013  (Isabelle2013)
+  http://isabelle.in.tum.de/cygwin_2013-1  (Isabelle2013-1)
 
 * Quasi-component: "isabelle makedist_cygwin"
 
diff -r aeb3cf02c678 -r cee071d33161 Admin/components/bundled-windows
--- a/Admin/components/bundled-windows	Mon Sep 16 16:48:08 2013 +0200
+++ b/Admin/components/bundled-windows	Mon Sep 16 19:30:33 2013 +0200
@@ -1,3 +1,3 @@
 #additional components to be bundled for release
-cygwin-20130117
+cygwin-20130916
 windows_app-20130909
diff -r aeb3cf02c678 -r cee071d33161 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Sep 16 16:48:08 2013 +0200
+++ b/Admin/components/components.sha1	Mon Sep 16 19:30:33 2013 +0200
@@ -3,6 +3,7 @@
 cb3b0706d208f104b800267697204f6d82f7b48a  cygwin-20130114.tar.gz
 3b44cca04855016d5f8cfb5101b2e0579ab80197  cygwin-20130117.tar.gz
 1fde9ddf0fa4f398965113d0c0c4f0e97c78d008  cygwin-20130716.tar.gz
+a03735a53c2963eb0b453f6a7282d3419f28bf38  cygwin-20130916.tar.gz
 0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
 2e293256a134eb8e5b1a283361b15eb812fbfbf1  e-1.6-1.tar.gz
 e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
diff -r aeb3cf02c678 -r cee071d33161 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Mon Sep 16 16:48:08 2013 +0200
+++ b/Admin/isatest/isatest-makedist	Mon Sep 16 19:30:33 2013 +0200
@@ -113,7 +113,8 @@
   $MAKEALL $HOME/settings/mac-poly64-M8;
   $MAKEALL $HOME/settings/mac-poly-M4;
   $MAKEALL $HOME/settings/mac-poly-M8;
-  $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs"
+  $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs;
+  $MAKEALL $HOME/settings/mac-poly-M8-quick_and_dirty"
 sleep 15
 $SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
 sleep 15
diff -r aeb3cf02c678 -r cee071d33161 Admin/isatest/settings/at-sml-dev-e
--- a/Admin/isatest/settings/at-sml-dev-e	Mon Sep 16 16:48:08 2013 +0200
+++ b/Admin/isatest/settings/at-sml-dev-e	Mon Sep 16 19:30:33 2013 +0200
@@ -3,7 +3,7 @@
 init_components /home/isabelle/contrib "$HOME/admin/components/main"
 
 ML_SYSTEM=smlnj
-ML_HOME="/home/smlnj/110.75/bin"
+ML_HOME="/home/smlnj/110.76/bin"
 ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
 
diff -r aeb3cf02c678 -r cee071d33161 Admin/isatest/settings/mac-poly-M8-quick_and_dirty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/settings/mac-poly-M8-quick_and_dirty	Mon Sep 16 19:30:33 2013 +0200
@@ -0,0 +1,31 @@
+# -*- shell-script -*- :mode=shellscript:
+
+init_components /home/isabelle/contrib "$HOME/admin/components/main"
+
+  POLYML_HOME="/home/polyml/polyml-5.5.0"
+  ML_SYSTEM="polyml-5.5.0"
+  ML_PLATFORM="x86-darwin"
+  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+  ML_OPTIONS="-H 1000 --gcthreads 8"
+
+
+ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-quick_and_dirty
+
+# 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_BUILD_OPTIONS="threads=8 quick_and_dirty"
+
+Z3_NON_COMMERCIAL="yes"
+
diff -r aeb3cf02c678 -r cee071d33161 Admin/lib/Tools/makedist_cygwin
--- a/Admin/lib/Tools/makedist_cygwin	Mon Sep 16 16:48:08 2013 +0200
+++ b/Admin/lib/Tools/makedist_cygwin	Mon Sep 16 19:30:33 2013 +0200
@@ -4,7 +4,7 @@
 
 ## global parameters
 
-CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2013"
+CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2013-1"
 
 
 ## diagnostics
@@ -43,7 +43,7 @@
 [ ! -e "$TARGET" ] || fail "Target already exists: \"$TARGET\""
 mkdir -p "$TARGET/isabelle" || fail "Failed to create target directory: \"$TARGET\""
 
-perl -MLWP::Simple -e "getprint '$CYGWIN_MIRROR/setup.exe';" > "$TARGET/isabelle/cygwin.exe"
+perl -MLWP::Simple -e "getprint '$CYGWIN_MIRROR/setup-x86.exe';" > "$TARGET/isabelle/cygwin.exe"
 chmod +x "$TARGET/isabelle/cygwin.exe"
 
 "$TARGET/isabelle/cygwin.exe" -h </dev/null >/dev/null || exit 2
@@ -55,7 +55,7 @@
   --site "$CYGWIN_MIRROR" --no-verify \
   --local-package-dir 'C:\temp' \
   --root "$(cygpath -w "$TARGET")" \
-  --packages libgmp3,make,perl,python,rlwrap,vim \
+  --packages libgmp3,perl,python,rlwrap,vim \
   --no-shortcuts --no-startmenu --no-desktop --quiet-mode
 
 [ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
diff -r aeb3cf02c678 -r cee071d33161 Admin/mira.py
--- a/Admin/mira.py	Mon Sep 16 16:48:08 2013 +0200
+++ b/Admin/mira.py	Mon Sep 16 19:30:33 2013 +0200
@@ -324,7 +324,7 @@
 
 smlnj_settings = '''
 ML_SYSTEM=smlnj
-ML_HOME="/home/smlnj/110.74/bin"
+ML_HOME="/home/smlnj/110.76/bin"
 ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
 '''
diff -r aeb3cf02c678 -r cee071d33161 NEWS
--- a/NEWS	Mon Sep 16 16:48:08 2013 +0200
+++ b/NEWS	Mon Sep 16 19:30:33 2013 +0200
@@ -128,6 +128,9 @@
 
 *** Pure ***
 
+* Former global reference trace_unify_fail is now available as
+configuration option "unify_trace_failure" (global context only).
+
 * Type theory is now immutable, without any special treatment of
 drafts or linear updates (which could lead to "stale theory" errors in
 the past).  Discontinued obsolete operations like Theory.copy,
diff -r aeb3cf02c678 -r cee071d33161 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Mon Sep 16 16:48:08 2013 +0200
+++ b/lib/scripts/run-polyml	Mon Sep 16 19:30:33 2013 +0200
@@ -52,7 +52,11 @@
   COMMIT='fun commit () = false;'
   MLEXIT=""
 else
-  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  if [ -z "$INFILE" ]; then
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  else
+    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+  fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   MLEXIT="commit();"
 fi
diff -r aeb3cf02c678 -r cee071d33161 lib/scripts/run-polyml-5.5.1
--- a/lib/scripts/run-polyml-5.5.1	Mon Sep 16 16:48:08 2013 +0200
+++ b/lib/scripts/run-polyml-5.5.1	Mon Sep 16 19:30:33 2013 +0200
@@ -53,7 +53,11 @@
   COMMIT='fun commit () = false;'
   MLEXIT=""
 else
-  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  if [ -z "$INFILE" ]; then
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  else
+    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+  fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   MLEXIT="commit();"
 fi
diff -r aeb3cf02c678 -r cee071d33161 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Mon Sep 16 16:48:08 2013 +0200
+++ b/lib/scripts/run-smlnj	Mon Sep 16 19:30:33 2013 +0200
@@ -47,6 +47,8 @@
 check_mlhome_file "$SML"
 check_mlhome_file "$ARCH_N_OPSYS"
 
+eval $("$ARCH_N_OPSYS")
+
 
 
 ## prepare databases
@@ -63,7 +65,11 @@
   COMMIT='fun commit () = false;'
   MLEXIT=""
 else
-  COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");"
+  if [ -z "$INFILE" ]; then
+    COMMIT="fun commit () = if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};"
+  else
+    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+  fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   MLEXIT="commit();"
 fi
@@ -87,11 +93,7 @@
 ## fix heap file name and permissions
 
 if [ -n "$OUTFILE" ]; then
-  eval $("$ARCH_N_OPSYS")
-  [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS"
-  HEAP="$OUTFILE.$HEAP_SUFFIX"
-  check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \
-    [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+  check_heap_file "$OUTFILE" && [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 fi
 
 exit "$RC"
diff -r aeb3cf02c678 -r cee071d33161 src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 16 16:48:08 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 16 19:30:33 2013 +0200
@@ -1,29 +1,33 @@
 (*  Title:      HOL/Tools/Function/fun_cases.ML
     Author:     Manuel Eberl, TU Muenchen
 
-Provides the fun_cases command for generating specialised elimination
+Provide the fun_cases command for generating specialised elimination
 rules for function package functions.
 *)
 
 signature FUN_CASES =
 sig
-  val mk_fun_cases : local_theory -> term -> thm
+  val mk_fun_cases : Proof.context -> term -> thm
+  val fun_cases_cmd: ((binding * Args.src list) * string list) list -> local_theory ->
+    (string * thm list) list * local_theory
+  (* FIXME regular ML interface for fun_cases *)
 end;
 
-
 structure Fun_Cases : FUN_CASES =
 struct
 
 local
 
-  val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
-    (fn _ => assume_tac 1);
-  val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
-  val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
+val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
+  (fn _ => assume_tac 1);
+val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
+val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
 
-  fun simp_case_tac ctxt i =
-    EVERY' [elim_tac, TRY o asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
+fun simp_case_tac ctxt i =
+  EVERY' [elim_tac, TRY o asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
+
 in
+
 fun mk_fun_cases ctxt prop =
   let val thy = Proof_Context.theory_of ctxt;
       fun err () =
@@ -32,7 +36,7 @@
            Pretty.fbrk, Syntax.pretty_term ctxt prop]));
       val ((f,_),_) = Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
               handle TERM _ => err ();
-      val info = Function.get_info ctxt f handle Empty => err ();
+      val info = Function.get_info ctxt f handle List.Empty => err ();
       val {elims, pelims, is_partial, ...} = info;
       val elims = if is_partial then pelims else the elims
       val cprop = cterm_of thy prop;
@@ -45,45 +49,52 @@
       SOME r => r
     | NONE => err ()
   end;
+
 end;
 
 
 (* Setting up the fun_cases command *)
+
 local
-  (* Converts the schematic variables and type variables in a term into free
-     variables and takes care of schematic variables originating from dummy
-     patterns by renaming them to something sensible. *)
-  fun pat_to_term ctxt t =
-    let
-       fun prep_var ((x,_),T) =
-            if x = "_dummy_" then ("x",T) else (x,T);
-       val schem_vars = Term.add_vars t [];
-       val prepped_vars = map prep_var schem_vars;
-       val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars);
-       val subst = ListPair.zip (map fst schem_vars, fresh_vars);
-    in fst (yield_singleton (Variable.import_terms true)
-           (subst_Vars subst t) ctxt)
-    end;
+
+(* Convert the schematic variables and type variables in a term into free
+   variables and takes care of schematic variables originating from dummy
+   patterns by renaming them to something sensible. *)
+fun pat_to_term ctxt t =
+  let
+     fun prep_var ((x,_),T) =
+          if x = "_dummy_" then ("x",T) else (x,T);
+     val schem_vars = Term.add_vars t [];
+     val prepped_vars = map prep_var schem_vars;
+     val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars);
+     val subst = ListPair.zip (map fst schem_vars, fresh_vars);
+  in fst (yield_singleton (Variable.import_terms true)
+         (subst_Vars subst t) ctxt)
+  end;
 
-  fun fun_cases args ctxt =
-    let
-      val thy = Proof_Context.theory_of ctxt
-      val thmss = map snd args
-                  |> burrow (grouped 10 Par_List.map
-                      (mk_fun_cases ctxt
-                       o pat_to_term ctxt
-                       o HOLogic.mk_Trueprop
-                       o Proof_Context.read_term_pattern ctxt));
-      val facts = map2 (fn ((a,atts), _) => fn thms =>
-        ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss;
-    in
-      ctxt |> Local_Theory.notes facts |>> map snd
-    end;
 in
+
+fun fun_cases_cmd args lthy =
+  let
+    val thy = Proof_Context.theory_of lthy
+    val thmss = map snd args
+                |> burrow (grouped 10 Par_List.map
+                    (mk_fun_cases lthy
+                     o pat_to_term lthy
+                     o HOLogic.mk_Trueprop
+                     o Proof_Context.read_term_pattern lthy));
+    val facts = map2 (fn ((a,atts), _) => fn thms =>
+      ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss;
+  in
+    lthy |> Local_Theory.notes facts
+  end;
+
 val _ =
   Outer_Syntax.local_theory @{command_spec "fun_cases"}
     "automatic derivation of simplified elimination rules for function equations"
-    (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases));
-end;
+    (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
+
 end;
 
+end;
+
diff -r aeb3cf02c678 -r cee071d33161 src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Mon Sep 16 16:48:08 2013 +0200
+++ b/src/HOL/Tools/Function/function_elims.ML	Mon Sep 16 19:30:33 2013 +0200
@@ -1,21 +1,21 @@
 (*  Title:      HOL/Tools/Function/function_elims.ML
     Author:     Manuel Eberl, TU Muenchen
 
-Generates the pelims rules for a function. These are of the shape
-[|f x y z = w; !!…. [|x = …; y = …; z = …; w = …|] ==> P; …|] ==> P
+Generate the pelims rules for a function. These are of the shape
+[|f x y z = w; !!\<dots>. [|x = \<dots>; y = \<dots>; z = \<dots>; w = \<dots>|] ==> P; \<dots>|] ==> P
 and are derived from the cases rule. There is at least one pelim rule for
 each function (cf. mutually recursive functions)
 There may be more than one pelim rule for a function in case of functions
 that return a boolean. For such a function, e.g. P x, not only the normal
 elim rule with the premise P x = z is generated, but also two additional
-elim rules with P x resp. ¬P x as premises.
+elim rules with P x resp. \<not>P x as premises.
 *)
 
 signature FUNCTION_ELIMS =
 sig
   val dest_funprop : term -> (term * term list) * term
-  val mk_partial_elim_rules :
-          local_theory -> Function_Common.function_result -> thm list list
+  val mk_partial_elim_rules : Proof.context ->
+    Function_Common.function_result -> thm list list
 end;
 
 structure Function_Elims : FUNCTION_ELIMS =
@@ -24,127 +24,132 @@
 open Function_Lib
 open Function_Common
 
-(* Extracts a function and its arguments from a proposition that is
+(* Extract a function and its arguments from a proposition that is
    either of the form "f x y z = ..." or, in case of function that
    returns a boolean, "f x y z" *)
-fun dest_funprop (Const ("HOL.eq", _) $ lhs $ rhs) = (strip_comb lhs, rhs)
-  | dest_funprop (Const ("HOL.Not", _) $ trm) = (strip_comb trm, @{term "False"})
+fun dest_funprop (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = (strip_comb lhs, rhs)
+  | dest_funprop (Const (@{const_name Not}, _) $ trm) = (strip_comb trm, @{term "False"})
   | dest_funprop trm = (strip_comb trm, @{term "True"});
 
 local
-  fun propagate_tac i thm =
-    let fun inspect eq = case eq of
-                Const ("HOL.Trueprop",_) $ (Const ("HOL.eq",_) $ Free x $ t) =>
-                    if Logic.occs (Free x, t) then raise Match else true
-              | Const ("HOL.Trueprop",_) $ (Const ("HOL.eq",_) $ t $ Free x) =>
-                    if Logic.occs (Free x, t) then raise Match else false
-              | _ => raise Match;
-        fun mk_eq thm = (if inspect (prop_of thm) then
-                            [thm RS eq_reflection]
-                        else
-                            [Thm.symmetric (thm RS eq_reflection)])
-                        handle Match => [];
-        val ss = Simplifier.global_context (Thm.theory_of_thm thm) empty_ss
-                 |> Simplifier.set_mksimps (K mk_eq)
-    in
-      asm_lr_simp_tac ss i thm
-    end;
+
+fun propagate_tac i thm =
+  let fun inspect eq = case eq of
+              Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) =>
+                  if Logic.occs (Free x, t) then raise Match else true
+            | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) =>
+                  if Logic.occs (Free x, t) then raise Match else false
+            | _ => raise Match;
+      fun mk_eq thm = (if inspect (prop_of thm) then
+                          [thm RS eq_reflection]
+                      else
+                          [Thm.symmetric (thm RS eq_reflection)])
+                      handle Match => [];
+      val ss = Simplifier.global_context (Thm.theory_of_thm thm) empty_ss
+               |> Simplifier.set_mksimps (K mk_eq)
+  in
+    asm_lr_simp_tac ss i thm
+  end;
 
-  val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+}
-  val boolE = @{thms HOL.TrueE HOL.FalseE}
-  val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+}
-  val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False}
+val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+}
+val boolE = @{thms HOL.TrueE HOL.FalseE}
+val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+}
+val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False}
 
-  fun bool_subst_tac ctxt i =
-      REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i)
-      THEN REPEAT (dresolve_tac boolD i)
-      THEN REPEAT (eresolve_tac boolE i)
+fun bool_subst_tac ctxt i =
+    REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i)
+    THEN REPEAT (dresolve_tac boolD i)
+    THEN REPEAT (eresolve_tac boolE i)
 
-  fun mk_bool_elims ctxt elim =
-    let val tac = ALLGOALS (bool_subst_tac ctxt)
-        fun mk_bool_elim b =
-          elim
-          |> Thm.forall_elim b
-          |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1))
-          |> Tactic.rule_by_tactic ctxt tac
-    in
-        map mk_bool_elim [@{cterm True}, @{cterm False}]
-    end;
+fun mk_bool_elims ctxt elim =
+  let val tac = ALLGOALS (bool_subst_tac ctxt)
+      fun mk_bool_elim b =
+        elim
+        |> Thm.forall_elim b
+        |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1))
+        |> Tactic.rule_by_tactic ctxt tac
+  in
+      map mk_bool_elim [@{cterm True}, @{cterm False}]
+  end;
 
 in
 
-  fun mk_partial_elim_rules ctxt result=
-    let val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
-                            termination, domintros, ...} = result;
-        val n_fs = length fs;
+fun mk_partial_elim_rules ctxt result =
+  let
+      val thy = Proof_Context.theory_of ctxt;
 
-        fun mk_partial_elim_rule (idx,f) =
-          let fun mk_funeq 0 T (acc_vars, acc_lhs) =
-                  let val y = Free("y",T) in
-                    (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T)
-                  end
-                | mk_funeq n (Type("fun",[S,T])) (acc_vars, acc_lhs) =
-                  let val xn = Free ("x" ^ Int.toString n,S) in
-                    mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn)
-                  end
-                | mk_funeq _ _ _ = raise (TERM ("Not a function.", [f]))
+      val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
+                          termination, domintros, ...} = result;
+      val n_fs = length fs;
 
-              val f_simps = filter (fn r => (prop_of r |> Logic.strip_assums_concl
-                                             |> HOLogic.dest_Trueprop
-                                             |> dest_funprop |> fst |> fst) = f)
-                                   psimps
+      fun mk_partial_elim_rule (idx,f) =
+        let fun mk_funeq 0 T (acc_vars, acc_lhs) =
+                let val y = Free("y",T) in
+                  (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T)
+                end
+              | mk_funeq n (Type(@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) =
+                let val xn = Free ("x" ^ Int.toString n,S) in
+                  mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn)
+                end
+              | mk_funeq _ _ _ = raise (TERM ("Not a function.", [f]))
 
-              val arity = hd f_simps |> prop_of |> Logic.strip_assums_concl
-                                     |> HOLogic.dest_Trueprop
-                                     |> snd o fst o dest_funprop |> length;
-              val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([],f)
-              val (rhs_var, arg_vars) = case free_vars of x::xs => (x, rev xs)
-              val args = HOLogic.mk_tuple arg_vars;
-              val domT = R |> dest_Free |> snd |> hd o snd o dest_Type
+            val f_simps = filter (fn r => (prop_of r |> Logic.strip_assums_concl
+                                           |> HOLogic.dest_Trueprop
+                                           |> dest_funprop |> fst |> fst) = f)
+                                 psimps
 
-              val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
+            val arity = hd f_simps |> prop_of |> Logic.strip_assums_concl
+                                   |> HOLogic.dest_Trueprop
+                                   |> snd o fst o dest_funprop |> length;
+            val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([],f)
+            val (rhs_var, arg_vars) = case free_vars of x::xs => (x, rev xs)
+            val args = HOLogic.mk_tuple arg_vars;
+            val domT = R |> dest_Free |> snd |> hd o snd o dest_Type
 
-              val thy = Proof_Context.theory_of ctxt;
-              val cprop = cterm_of thy prop
+            val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
 
-              val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
-              val asms_thms = map Thm.assume asms;
+            val cprop = cterm_of thy prop
 
-              fun prep_subgoal i =
-                REPEAT (eresolve_tac @{thms Pair_inject} i)
-                THEN Method.insert_tac (case asms_thms of
-                                          thm::thms => (thm RS sym) :: thms) i
-                THEN propagate_tac i
-                THEN TRY
-                    ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
-                THEN bool_subst_tac ctxt i;
+            val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
+            val asms_thms = map Thm.assume asms;
 
-            val tac = ALLGOALS prep_subgoal;
+            fun prep_subgoal i =
+              REPEAT (eresolve_tac @{thms Pair_inject} i)
+              THEN Method.insert_tac (case asms_thms of
+                                        thm::thms => (thm RS sym) :: thms) i
+              THEN propagate_tac i
+              THEN TRY
+                  ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
+              THEN bool_subst_tac ctxt i;
+
+          val tac = ALLGOALS prep_subgoal;
 
-            val elim_stripped =
-                  nth cases idx
-                  |> Thm.forall_elim @{cterm "P::bool"}
-                  |> Thm.forall_elim (cterm_of thy args)
-                  |> Tactic.rule_by_tactic ctxt tac
-                  |> fold_rev Thm.implies_intr asms
-                  |> Thm.forall_intr (cterm_of thy rhs_var)
+          val elim_stripped =
+                nth cases idx
+                |> Thm.forall_elim @{cterm "P::bool"}
+                |> Thm.forall_elim (cterm_of thy args)
+                |> Tactic.rule_by_tactic ctxt tac
+                |> fold_rev Thm.implies_intr asms
+                |> Thm.forall_intr (cterm_of thy rhs_var)
 
-            val bool_elims = (case ranT of
-                                Type ("HOL.bool", []) => mk_bool_elims ctxt elim_stripped
-                                | _ => []);
+          val bool_elims = (case ranT of
+                              Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
+                              | _ => []);
 
-            fun unstrip rl =
-                  rl  |> (fn thm => List.foldr (uncurry Thm.forall_intr) thm
-                             (map (cterm_of thy) arg_vars))
-                      |> Thm.forall_intr @{cterm "P::bool"}
+          fun unstrip rl =
+                rl  |> (fn thm => List.foldr (uncurry Thm.forall_intr) thm
+                           (map (cterm_of thy) arg_vars))
+                    |> Thm.forall_intr @{cterm "P::bool"}
 
-        in
-          map unstrip (elim_stripped :: bool_elims)
-        end;
+      in
+        map unstrip (elim_stripped :: bool_elims)
+      end;
 
-    in
-      map_index mk_partial_elim_rule fs
-    end;
+  in
+    map_index mk_partial_elim_rule fs
   end;
+
 end;
 
+end;
+
diff -r aeb3cf02c678 -r cee071d33161 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Sep 16 16:48:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Sep 16 19:30:33 2013 +0200
@@ -71,10 +71,10 @@
     val assms = assms |> map (Display.pretty_thm ctxt)
                       |> (fn [] => Pretty.str ""
                            | [a] => a
-                           | assms => Pretty.enum ";" "⟦" "⟧" assms)
+                           | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms)  (* Syntax.pretty_term!? *)
     val concl = concl |> Syntax.pretty_term ctxt
     val trace_list = [] |> cons concl
-                        |> nr_of_assms>0 ? cons (Pretty.str "⟹")
+                        |> nr_of_assms>0 ? cons (Pretty.str "\<Longrightarrow>")
                         |> cons assms
                         |> cons time
     val pretty_trace = Pretty.blk(2, Pretty.breaks trace_list)
diff -r aeb3cf02c678 -r cee071d33161 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Sep 16 16:48:08 2013 +0200
+++ b/src/Pure/Tools/build.scala	Mon Sep 16 19:30:33 2013 +0200
@@ -441,8 +441,22 @@
             (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
               info.files.map(file => info.dir + file)).map(_.expand)
 
-          if (list_files)
+          if (list_files) {
             progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
+            for {
+              file <- all_files
+              if file.split_ext._2 == "ML"
+            } {
+              val path = info.dir + file
+              try { Symbol.decode_strict(File.read(path)) }
+              catch {
+                case ERROR(msg) =>
+                  cat_error(msg,
+                    "The error(s) above occurred in session " + quote(name) +
+                      " file " + path.toString)
+              }
+            }
+          }
 
           val sources =
             try { all_files.map(p => (p, SHA1.digest(p.file))) }