--- a/src/HOL/TPTP/MaSh_Import.thy	Tue Jul 17 23:11:27 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Import.thy	Wed Jul 18 08:44:03 2012 +0200
@@ -9,6 +9,10 @@
 uses "mash_import.ML"
 begin
 
+sledgehammer_params
+  [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
+   lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
+
 declare [[sledgehammer_instantiate_inducts]]
 
 ML {*