1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Mon Jun 02 11:59:49 2014 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Mon Jun 02 11:59:50 2014 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
     1.5     lam_trans = lifting, timeout = 2, dont_preplay, minimize]
     1.6  
     1.7 +declare [[sledgehammer_fact_duplicates = true]]
     1.8  declare [[sledgehammer_instantiate_inducts = false]]
     1.9  
    1.10  hide_fact (open) HOL.ext