1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 25 23:02:50 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jul 26 10:48:03 2012 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4  val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
     1.5  val prover = hd provers
     1.6  *}
     1.7 -
     1.8  ML {*
     1.9  if do_it then
    1.10    generate_accessibility thy false "/tmp/mash_accessibility"
    1.11 @@ -47,7 +46,7 @@
    1.12  
    1.13  ML {*
    1.14  if do_it then
    1.15 -  generate_commands @{context} prover thy "/tmp/mash_commands"
    1.16 +  generate_commands @{context} params thy "/tmp/mash_commands"
    1.17  else
    1.18    ()
    1.19  *}