# HG changeset patch
# User blanchet
# Date 1344009395 -7200
# Node ID 81755fd809be23de2d84a6670b039e279633289b
# Parent  49c080255a57ca675c44cd0fa988bc7d1f73628d
never use MaSh in Metis examples, to avoid one dimension of nondeterminism

diff -r 49c080255a57 -r 81755fd809be src/HOL/Metis_Examples/Type_Encodings.thy
--- 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 *}