--- a/src/HOL/TPTP/MaSh_Eval.thy Fri Jun 27 19:17:16 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy Fri Jun 27 19:21:58 2014 +0200
@@ -14,6 +14,7 @@
[provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
lam_trans = lifting, timeout = 15, dont_preplay, minimize]
+declare [[sledgehammer_fact_duplicates = true]]
declare [[sledgehammer_instantiate_inducts = false]]
ML {*
@@ -28,7 +29,6 @@
val do_it = false (* switch to "true" to generate the files *)
val params = Sledgehammer_Commands.default_params @{theory} []
val range = (1, NONE)
-val linearize = false
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
val prob_dir = prefix ^ "mash_problems"
@@ -43,7 +43,7 @@
ML {*
if do_it then
- evaluate_mash_suggestions @{context} params range linearize
+ evaluate_mash_suggestions @{context} params range
[MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
(SOME prob_dir)
(prefix ^ "mepo_suggestions")