| changeset 48379 | 2b5ad61e2ccc |
| parent 48333 | 2250197977dc |
| child 48432 | 60759d07df24 |
--- a/src/HOL/TPTP/MaSh_Export.thy Fri Jul 20 22:19:45 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Fri Jul 20 22:19:45 2012 +0200 @@ -54,7 +54,7 @@ ML {* if do_it then - generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions" + generate_mepo_suggestions @{context} params thy 500 "/tmp/mash_mepo_suggestions" else () *}