--- a/src/HOL/TPTP/MaSh_Export.thy Thu Dec 13 15:39:07 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Thu Dec 13 22:49:06 2012 +0100
@@ -11,12 +11,16 @@
ML_file "mash_export.ML"
sledgehammer_params
- [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native,
+ [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize]
declare [[sledgehammer_instantiate_inducts]]
ML {*
+!Multithreading.max_threads
+*}
+
+ML {*
open MaSh_Export
*}