diff -r af1dabad14c0 -r 716ec3458b1d src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 25 23:02:50 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jul 26 10:48:03 2012 +0200
@@ -23,7 +23,6 @@
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
 *}
-
 ML {*
 if do_it then
   generate_accessibility thy false "/tmp/mash_accessibility"
@@ -47,7 +46,7 @@
 
 ML {*
 if do_it then
-  generate_commands @{context} prover thy "/tmp/mash_commands"
+  generate_commands @{context} params thy "/tmp/mash_commands"
 else
   ()
 *}