author | blanchet |
Thu, 10 Jan 2013 23:48:01 +0100 | |
changeset 50816 | 2c366a03c888 |
parent 50815 | 41b804049fae |
child 50817 | 652731d92061 |
--- 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