diff -r 7a7d1418301e -r b85cb3049df9 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 23:29:22 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 23:53:55 2013 +0100
@@ -105,4 +105,12 @@
   ()
 *}
 
+ML {*
+if do_it then
+  generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions")
+      (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
+else
+  ()
+*}
+
 end