diff -r 6666fc0b9ebc -r 42c209a6c225 src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Dec 11 18:02:22 2013 +0100
@@ -17,7 +17,7 @@
 declare [[sledgehammer_instantiate_inducts = false]]
 
 ML {*
-!Multithreading.max_threads
+Multithreading.max_threads_value ()
 *}
 
 ML {*