# HG changeset patch
# User blanchet
# Date 1400756871 -7200
# Node ID b1ae5079b7957cc55b6c72b782ed6b772a512153
# Parent  e54713f22a88cc5849086488abd3b5b88a1f6a63
make MaSh Python the default when passing 'fact_filter = mash' without enabling the 'maSh' Isabelle system option

diff -r e54713f22a88 -r b1ae5079b795 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu May 22 09:40:05 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu May 22 13:07:51 2014 +0200
@@ -128,7 +128,7 @@
   end
 
 val is_mash_enabled = is_some o mash_engine
-val the_mash_engine = the_default MaSh_SML_kNN o mash_engine
+val the_mash_engine = the_default MaSh_Py o mash_engine
 
 
 (*** Low-level communication with Python version of MaSh ***)
@@ -534,7 +534,8 @@
     val num_visible_facts = length visible_facts
     val get_deps = curry Vector.sub deps_vec
   in
-    trace_msg ctxt (fn () => "MaSh_SML query " ^ encode_features feats ^ " from {" ^
+    trace_msg ctxt (fn () => "MaSh_SML " ^ (if engine = MaSh_SML_kNN then "kNN" else "NB") ^
+      " query " ^ encode_features feats ^ " from {" ^
       elide_string 1000 (space_implode " " (take num_visible_facts facts)) ^ "}");
     (if engine = MaSh_SML_kNN then
        let