1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:05 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:05 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* MaSh Exporter *}
     1.5  
     1.6  theory MaSh_Export
     1.7 -imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
     1.8 +imports Complex_Main
     1.9  uses "mash_export.ML"
    1.10  begin
    1.11  
    1.12 @@ -18,9 +18,10 @@
    1.13  *}
    1.14  
    1.15  ML {*
    1.16 -val do_it = false (* switch to "true" to generate the files *);
    1.17 -val thy = @{theory List};
    1.18 -val params = Sledgehammer_Isar.default_params @{context} []
    1.19 +val do_it = false (* switch to "true" to generate the files *)
    1.20 +val thy = @{theory List}
    1.21 +val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
    1.22 +val prover = hd provers
    1.23  *}
    1.24  
    1.25  ML {*
    1.26 @@ -32,14 +33,28 @@
    1.27  
    1.28  ML {*
    1.29  if do_it then
    1.30 -  generate_features @{context} thy false "/tmp/mash_features"
    1.31 +  generate_features @{context} prover thy false "/tmp/mash_features"
    1.32  else
    1.33    ()
    1.34  *}
    1.35  
    1.36  ML {*
    1.37  if do_it then
    1.38 -  generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
    1.39 +  generate_isar_dependencies thy false "/tmp/mash_dependencies"
    1.40 +else
    1.41 +  ()
    1.42 +*}
    1.43 +
    1.44 +ML {*
    1.45 +if do_it then
    1.46 +  generate_commands @{context} prover thy "/tmp/mash_commands"
    1.47 +else
    1.48 +  ()
    1.49 +*}
    1.50 +
    1.51 +ML {*
    1.52 +if do_it then
    1.53 +  generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
    1.54  else
    1.55    ()
    1.56  *}
    1.57 @@ -51,18 +66,5 @@
    1.58    ()
    1.59  *}
    1.60  
    1.61 -ML {*
    1.62 -if do_it then
    1.63 -  generate_commands @{context} thy "/tmp/mash_commands"
    1.64 -else
    1.65 -  ()
    1.66 -*}
    1.67 -
    1.68 -ML {*
    1.69 -if do_it then
    1.70 -  generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
    1.71 -else
    1.72 -  ()
    1.73 -*}
    1.74  
    1.75  end