--- 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