1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Sat Dec 15 21:26:10 2012 +0100
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Sat Dec 15 21:34:32 2012 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4  
     1.5  ML {*
     1.6  if do_it then
     1.7 -  generate_prover_dependencies @{context} params thys false
     1.8 +  generate_prover_dependencies @{context} params (1, NONE) thys false
     1.9        (prefix ^ "mash_prover_dependencies")
    1.10  else
    1.11    ()
    1.12 @@ -87,7 +87,7 @@
    1.13  
    1.14  ML {*
    1.15  if do_it then
    1.16 -  generate_prover_commands @{context} params thys
    1.17 +  generate_prover_commands @{context} params (1, NONE) thys
    1.18        (prefix ^ "mash_prover_commands")
    1.19  else
    1.20    ()