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