src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

     Proof.context -> bool -> (string * string list) list -> unit
   val mash_QUERY :
     Proof.context -> bool -> int -> string list * string list
     -> (string * real) list
   val mash_unlearn : Proof.context -> unit
-  val mash_could_suggest_facts : unit -> bool
+  val is_mash_enabled : unit -> bool
   val mash_can_suggest_facts : Proof.context -> bool
   val mash_suggested_facts :
     Proof.context -> params -> string -> int -> term list -> term
     -> fact list -> (fact * real) list * fact list
   val mash_learn_proof :

 val learn_isarN = "learn_isar"
 val learn_atpN = "learn_atp"
 val relearn_isarN = "relearn_isar"
 val relearn_atpN = "relearn_atp"
 
-fun is_mash_enabled () = (getenv "MASH" = "yes")
 fun mash_home () = getenv "ISABELLE_SLEDGEHAMMER_MASH"
 fun mash_model_dir () =
   getenv "ISABELLE_HOME_USER" ^ "/mash"
   |> tap (Isabelle_System.mkdir o Path.explode)
 val mash_state_dir = mash_model_dir

       (mash_CLEAR ctxt; (* also removes the state file *)
        (true, empty_state)))
 
 end
 
-fun mash_could_suggest_facts () = is_mash_enabled ()
+fun is_mash_enabled () = (getenv "MASH" = "yes")
 fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt)))
 
 fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
 
 fun maximal_in_graph fact_G facts =

         case fact_filter of
           SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
         | NONE =>
           if is_smt_prover ctxt prover then
             mepoN
-          else if mash_could_suggest_facts () then
+          else if is_mash_enabled () then
             (maybe_learn ();
              if mash_can_suggest_facts ctxt then meshN else mepoN)
           else
             mepoN
       val add_ths = Attrib.eval_thms ctxt add