1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 01 16:47:10 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 01 16:47:10 2014 +0200
     1.3 @@ -148,18 +148,18 @@
     1.4  fun mash_engine () =
     1.5    let val flag1 = Options.default_string @{system_option MaSh} in
     1.6      (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
     1.7 -      "yes" => SOME MaSh_NB
     1.8 -    | "sml" => SOME MaSh_NB
     1.9 +      "yes" => SOME MaSh_NB_kNN
    1.10 +    | "sml" => SOME MaSh_NB_kNN
    1.11      | "nb" => SOME MaSh_NB
    1.12      | "knn" => SOME MaSh_kNN
    1.13      | "nb_knn" => SOME MaSh_NB_kNN
    1.14      | "nb_ext" => SOME MaSh_NB_Ext
    1.15      | "knn_ext" => SOME MaSh_kNN_Ext
    1.16 -    | _ => NONE)
    1.17 +    | engine => (warning ("Unknown MaSh engine: " ^ quote engine ^ "."); NONE))
    1.18    end
    1.19  
    1.20  val is_mash_enabled = is_some o mash_engine
    1.21 -val the_mash_engine = the_default MaSh_NB o mash_engine
    1.22 +val the_mash_engine = the_default MaSh_NB_kNN o mash_engine
    1.23  
    1.24  fun scaled_avg [] = 0
    1.25    | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs