--- 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 {*