diff -r ac18480cbf9d -r 43d5f3d6d04e src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Aug 21 09:25:40 2013 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Aug 21 09:25:40 2013 +0200
@@ -71,16 +71,16 @@
 
 ML {*
 if do_it then
-  generate_isar_commands @{context} prover (range, step) thys
-      linearize (prefix ^ "mash_commands")
+  generate_isar_commands @{context} prover (range, step) thys linearize
+      max_suggestions (prefix ^ "mash_commands")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params (range, step) thys
-      linearize max_suggestions (prefix ^ "mepo_suggestions")
+  generate_mepo_suggestions @{context} params (range, step) thys linearize
+      max_suggestions (prefix ^ "mepo_suggestions")
 else
   ()
 *}
@@ -103,8 +103,8 @@
 
 ML {*
 if do_it then
-  generate_prover_commands @{context} params (range, step) thys
-      linearize (prefix ^ "mash_prover_commands")
+  generate_prover_commands @{context} params (range, step) thys linearize
+      max_suggestions (prefix ^ "mash_prover_commands")
 else
   ()
 *}