diff -r b88c3e0b752e -r 854a47677335 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 13:59:39 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
@@ -9,40 +9,66 @@
 uses "mash_export.ML"
 begin
 
-sledgehammer_params [provers = e, max_relevant = 500]
+sledgehammer_params
+  [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
+   lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
 
 ML {*
 open MaSh_Export
 *}
 
 ML {*
-val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory List}
+if do_it then
+  generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
+else
+  ()
 *}
 
 ML {*
-if do_it then generate_meng_paulson_suggestions @{context} thy "/tmp/mash_meng_paulson_suggestions"
-else ()
+val do_it = true (* switch to "true" to generate the files *);
+val thy = @{theory Nat}
 *}
 
 ML {*
-if do_it then generate_mash_commands thy "/tmp/mash_commands"
-else ()
+if do_it then
+  generate_features thy false "/tmp/mash_features"
+else
+  ()
 *}
 
 ML {*
-if do_it then generate_mash_features thy false "/tmp/mash_features"
-else ()
+if do_it then
+  generate_accessibility thy false "/tmp/mash_accessibility"
+else
+  ()
 *}
 
 ML {*
-if do_it then generate_mash_accessibility thy false "/tmp/mash_accessibility"
-else ()
+if do_it then
+  generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
+else
+  ()
 *}
 
 ML {*
-if do_it then generate_mash_dependencies thy false "/tmp/mash_dependencies"
-else ()
+if do_it then
+  generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_commands thy "/tmp/mash_commands"
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  generate_meng_paulson_suggestions @{context} thy 500 "/tmp/mash_meng_paulson_suggestions"
+else
+  ()
 *}
 
 end