1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 23:29:22 2013 +0100
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 23:53:55 2013 +0100
     1.3 @@ -105,4 +105,12 @@
     1.4    ()
     1.5  *}
     1.6  
     1.7 +ML {*
     1.8 +if do_it then
     1.9 +  generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions")
    1.10 +      (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
    1.11 +else
    1.12 +  ()
    1.13 +*}
    1.14 +
    1.15  end