--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon May 26 14:10:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon May 26 14:15:48 2014 +0200
@@ -117,7 +117,7 @@
datatype mash_engine = MaSh_Py | MaSh_SML_kNN | MaSh_SML_NB
fun mash_engine () =
- let val flag1 = Options.default_string @{system_option maSh} in
+ 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
| "py" => SOME MaSh_Py