1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  ML {*
     1.6  if do_it then
     1.7 -  generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
     1.8 +  generate_mepo_suggestions @{context} params thy 500 "/tmp/mash_mepo_suggestions"
     1.9  else
    1.10    ()
    1.11  *}