diff -r 923f1e199f4f -r c9023d78d1a6 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Dec 06 16:07:09 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Dec 06 16:49:48 2012 +0100
@@ -11,8 +11,8 @@
 ML_file "mash_export.ML"
 
 sledgehammer_params
-  [provers = spass, max_relevant = 40, strict, dont_slice, type_enc = mono_native,
-   lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize]
+  [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native,
+   lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize]
 
 ML {*
 open MaSh_Export
@@ -57,7 +57,7 @@
 
 ML {*
 if do_it then
-  generate_commands @{context} params thys (prefix ^ "mash_commands")
+  generate_isar_commands @{context} prover thys (prefix ^ "mash_commands")
 else
   ()
 *}
@@ -76,4 +76,11 @@
   ()
 *}
 
+ML {*
+if do_it then
+  generate_atp_commands @{context} params thys (prefix ^ "mash_atp_commands")
+else
+  ()
+*}
+
 end