changeset 50906 | 67b04a8375b0 |
parent 50816 | 2c366a03c888 |
child 50925 | dfc0177384f9 |
--- a/src/HOL/TPTP/MaSh_Export.thy Tue Jan 15 20:51:30 2013 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jan 16 12:46:11 2013 +0100 @@ -72,7 +72,7 @@ ML {* if do_it then - generate_mepo_suggestions @{context} params thys max_suggestions + generate_mepo_suggestions @{context} params (1, NONE) thys max_suggestions (prefix ^ "mepo_suggestions") else ()