--- 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
()
*}