# HG changeset patch
# User blanchet
# Date 1405376492 -7200
# Node ID 12fb55fc11a6ca35061a457360ef6ff576cbd517
# Parent  2a6c31ac1c9aad6342a5906cb6488dd00187812a
no warning in case MaSh is disabled

diff -r 2a6c31ac1c9a -r 12fb55fc11a6 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 15 00:21:32 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 15 00:21:32 2014 +0200
@@ -136,6 +136,7 @@
 | MaSh_NB_Ext
 | MaSh_kNN_Ext
 
+(* TODO: eliminate "MASH" environment variable after Isabelle2014 release *)
 fun mash_algorithm () =
   let val flag1 = Options.default_string @{system_option MaSh} in
     (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
@@ -146,6 +147,7 @@
     | "nb_knn" => SOME MaSh_NB_kNN
     | "nb_ext" => SOME MaSh_NB_Ext
     | "knn_ext" => SOME MaSh_kNN_Ext
+    | "" => NONE
     | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
   end