# HG changeset patch
# User blanchet
# Date 1380542666 -7200
# Node ID 62266b02197e4ef8aadb9c82a5d22c3d872ac936
# Parent  7297000915568ef9e87886b0640659a57f887a8b# Parent  1781bf24cdf187f9060579709c14b2e391d28713
merge

diff -r 1781bf24cdf1 -r 62266b02197e src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Mon Sep 30 11:20:24 2013 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Mon Sep 30 14:04:26 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 1781bf24cdf1 -r 62266b02197e src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Sep 30 11:20:24 2013 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Sep 30 14:04:26 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 1781bf24cdf1 -r 62266b02197e src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Sep 30 11:20:24 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Sep 30 14:04:26 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