src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

 datatype mash_engine = MaSh_Py | MaSh_SML_kNN | MaSh_SML_NB
 
 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_Py
+      "yes" => SOME MaSh_SML_NB
     | "py" => SOME MaSh_Py
     | "sml" => SOME MaSh_SML_NB
     | "sml_knn" => SOME MaSh_SML_kNN
     | "sml_nb" => SOME MaSh_SML_NB
     | _ => NONE)
   end
 
 val is_mash_enabled = is_some o mash_engine
-val the_mash_engine = the_default MaSh_Py o mash_engine
-
-
-(*** Low-level communication with Python version of MaSh ***)
+val the_mash_engine = the_default MaSh_SML_NB o mash_engine
+
+
+(*** Low-level communication with the Python version of MaSh ***)
 
 val save_models_arg = "--saveModels"
 val shutdown_server_arg = "--shutdownServer"
 
 fun wipe_out_file file = (try (File.rm o Path.explode) file; ())

       val (save, effective_fact_filter) =
         (case fact_filter of
           SOME ff => (ff <> mepoN andalso maybe_learn (), ff)
         | NONE =>
           if is_mash_enabled () then
-            (maybe_learn (),
-             if mash_can_suggest_facts ctxt overlord then meshN else mepoN)
+            (maybe_learn (), if mash_can_suggest_facts ctxt overlord then meshN else mepoN)
           else
             (false, mepoN))
 
       val unique_facts = drop_duplicate_facts facts
       val add_ths = Attrib.eval_thms ctxt add