never use MaSh in Metis examples, to avoid one dimension of nondeterminism

--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Fri Aug 03 16:27:38 2012 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Fri Aug 03 17:56:35 2012 +0200
@@ -14,7 +14,7 @@
 
 declare [[metis_new_skolemizer]]
 
-sledgehammer_params [prover = spass, blocking, timeout = 30,
+sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30,
                      preplay_timeout = 0, dont_minimize]
 
 text {* Setup for testing Metis exhaustively *}