diff -r 29efe682335b -r dabd4516450d src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Tue Jul 01 16:47:10 2014 +0200
+++ b/src/HOL/Tools/etc/options	Tue Jul 01 16:47:10 2014 +0200
@@ -36,4 +36,4 @@
   -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
 
 public option MaSh : string = "sml"
-  -- "machine learning engine to use by Sledgehammer (sml, nb, knn, none)"
+  -- "machine learning engine to use by Sledgehammer (nb_knn, nb, knn, none)"