changeset 50816 | 2c366a03c888 |
parent 50814 | 4247cbd78aaf |
child 50906 | 67b04a8375b0 |
--- a/src/HOL/TPTP/MaSh_Export.thy Thu Jan 10 23:34:20 2013 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jan 10 23:48:01 2013 +0100 @@ -71,7 +71,7 @@ *} ML {* -if true orelse do_it then +if do_it then generate_mepo_suggestions @{context} params thys max_suggestions (prefix ^ "mepo_suggestions") else