# HG changeset patch
# User wenzelm
# Date 1380543573 -7200
# Node ID c1097679e2955ad7460150e6c4aa8d573ce9b354
# Parent  62266b02197e4ef8aadb9c82a5d22c3d872ac936# Parent  1d457fc83f5cb7f71dc47caf8c211160254de30a
merged

diff -r 1d457fc83f5c -r c1097679e295 src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Mon Sep 30 14:17:27 2013 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Mon Sep 30 14:19:33 2013 +0200
@@ -14,6 +14,9 @@
 imports Type_Encodings
 begin
 
+sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30,
+                     preplay_timeout = 0, dont_minimize]
+
 text {* Extensionality and set constants *}
 
 lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
diff -r 1d457fc83f5c -r c1097679e295 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Sep 30 14:17:27 2013 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Sep 30 14:19:33 2013 +0200
@@ -14,9 +14,6 @@
 
 declare [[metis_new_skolem]]
 
-sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30,
-                     preplay_timeout = 0, dont_minimize]
-
 text {* Setup for testing Metis exhaustively *}
 
 lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
diff -r 1d457fc83f5c -r c1097679e295 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Sep 30 14:17:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Sep 30 14:19:33 2013 +0200
@@ -710,7 +710,7 @@
             SOME path => path
           | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
         end
-      | NONE => error ("The environment variable " ^ quote (hd (fst exec)) ^
+      | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^
                        " is not set.")
     fun split_time s =
       let