# HG changeset patch
# User blanchet
# Date 1404226030 -7200
# Node ID dabd4516450dbe192c81700732c6a06d382fcc10
# Parent  29efe682335be2e298041cac146701df3a7e28a0
changed default MaSh engine

diff -r 29efe682335b -r dabd4516450d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 01 16:47:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 01 16:47:10 2014 +0200
@@ -148,18 +148,18 @@
 fun mash_engine () =
   let val flag1 = Options.default_string @{system_option MaSh} in
     (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
-      "yes" => SOME MaSh_NB
-    | "sml" => SOME MaSh_NB
+      "yes" => SOME MaSh_NB_kNN
+    | "sml" => SOME MaSh_NB_kNN
     | "nb" => SOME MaSh_NB
     | "knn" => SOME MaSh_kNN
     | "nb_knn" => SOME MaSh_NB_kNN
     | "nb_ext" => SOME MaSh_NB_Ext
     | "knn_ext" => SOME MaSh_kNN_Ext
-    | _ => NONE)
+    | engine => (warning ("Unknown MaSh engine: " ^ quote engine ^ "."); NONE))
   end
 
 val is_mash_enabled = is_some o mash_engine
-val the_mash_engine = the_default MaSh_NB o mash_engine
+val the_mash_engine = the_default MaSh_NB_kNN o mash_engine
 
 fun scaled_avg [] = 0
   | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
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)"