diff -r f55c173a3cbc -r b246943b3aa3 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Thu Jul 24 18:46:38 2014 +0200
+++ b/src/HOL/Tools/etc/options	Thu Jul 24 18:46:38 2014 +0200
@@ -35,5 +35,5 @@
 public option z3_non_commercial : string = "unknown"
   -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
 
-public option MaSh : string = "none"
+public option MaSh : string = "sml"
   -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"