# HG changeset patch
# User blanchet
# Date 1353940263 -3600
# Node ID 78f3be5e51d2ff1a3888811163b6e41fc0f4c4d4
# Parent  cf1a274bbba600de8b97bb62c19a6023b0d4339a
simplify code slightly

diff -r cf1a274bbba6 -r 78f3be5e51d2 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Nov 26 15:31:03 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Nov 26 15:31:03 2012 +0100
@@ -55,7 +55,7 @@
     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
@@ -101,7 +101,6 @@
 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"
@@ -623,7 +622,7 @@
 
 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
@@ -974,7 +973,7 @@
         | 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