use SPASS instead of E for Metis examples -- it's seems faster for these small problems

--- a/src/HOL/Metis_Examples/Proxies.thy	Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Metis_Examples/Proxies.thy	Tue Feb 28 15:54:51 2012 +0100
@@ -51,10 +51,9 @@
 by linarith
 
 lemma "B \<le> C"
-sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some]
+sledgehammer [expect = some]
 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
 
-
 text {* Proxies for logical constants *}
 
 lemma "id (op =) x x"

--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Feb 28 15:54:51 2012 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Tue Feb 28 15:54:51 2012 +0100
@@ -14,7 +14,8 @@
 
 declare [[metis_new_skolemizer]]
 
-sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0]
+sledgehammer_params [prover = spass, blocking, timeout = 30,
+                     preplay_timeout = 0, dont_minimize]
 
 text {* Setup for testing Metis exhaustively *}