# HG changeset patch
# User blanchet
# Date 1380542347 -7200
# Node ID 7297000915568ef9e87886b0640659a57f887a8b
# Parent  16a0cd5293d9c100c6a8410d02768d55744acb69
minor tweak to error message

diff -r 16a0cd5293d9 -r 729700091556 src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Sun Sep 29 18:51:01 2013 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Mon Sep 30 13:59:07 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 16a0cd5293d9 -r 729700091556 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Sun Sep 29 18:51:01 2013 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Sep 30 13:59:07 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 16a0cd5293d9 -r 729700091556 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Sep 29 18:51:01 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Sep 30 13:59:07 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