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