1.1 --- a/src/HOL/TPTP/MaSh_Eval.thy	Mon Feb 18 18:34:55 2013 +0100
     1.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy	Tue Feb 19 13:21:49 2013 +0100
     1.3 @@ -28,6 +28,7 @@
     1.4  val do_it = false (* switch to "true" to generate the files *)
     1.5  val params = Sledgehammer_Isar.default_params @{context} []
     1.6  val range = (1, NONE)
     1.7 +val linearize = false
     1.8  val dir = "List"
     1.9  val prefix = "/tmp/" ^ dir ^ "/"
    1.10  val prob_dir = prefix ^ "mash_problems"
    1.11 @@ -42,7 +43,7 @@
    1.12  
    1.13  ML {*
    1.14  if do_it then
    1.15 -  evaluate_mash_suggestions @{context} params range
    1.16 +  evaluate_mash_suggestions @{context} params range linearize
    1.17        [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
    1.18        (SOME prob_dir)
    1.19        (prefix ^ "mepo_suggestions")