1.1 --- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Jul 18 08:44:05 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Jul 18 08:44:05 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* MaSh Evaluation Driver *}
     1.5  
     1.6  theory MaSh_Eval
     1.7 -imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d"
     1.8 +imports Complex_Main
     1.9  uses "mash_eval.ML"
    1.10  begin
    1.11  
    1.12 @@ -20,14 +20,14 @@
    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 Nat};
    1.18 +val do_it = false (* switch to "true" to generate the files *)
    1.19 +val thy = @{theory Nat}
    1.20  val params = Sledgehammer_Isar.default_params @{context} []
    1.21  *}
    1.22  
    1.23  ML {*
    1.24  if do_it then
    1.25 -  evaluate_mash_suggestions @{context} params thy "/Users/blanchet/tum/mash/mash/results/natNB200ATP-15.pred"
    1.26 +  evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions"
    1.27  else
    1.28    ()
    1.29  *}