--- 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"
--- 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
--- 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