| changeset 49394 | 2b5ad61e2ccc |
| parent 49348 | 2250197977dc |
| child 49447 | 60759d07df24 |
| 49393:9e96486d53ad | 49394:2b5ad61e2ccc |
|---|---|
52 () |
52 () |
53 *} |
53 *} |
54 |
54 |
55 ML {* |
55 ML {* |
56 if do_it then |
56 if do_it then |
57 generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions" |
57 generate_mepo_suggestions @{context} params thy 500 "/tmp/mash_mepo_suggestions" |
58 else |
58 else |
59 () |
59 () |
60 *} |
60 *} |
61 |
61 |
62 ML {* |
62 ML {* |