1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -564,7 +564,7 @@
     1.4    let
     1.5      val thy = Proof_Context.theory_of ctxt
     1.6      val prover = hd provers
     1.7 -    val name = ATP_Util.timestamp () ^ serial_string () (* fresh enough *)
     1.8 +    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
     1.9      val feats = features_of ctxt prover thy General [t]
    1.10      val deps = used_ths |> map Thm.get_name_hint
    1.11    in
    1.12 @@ -583,8 +583,7 @@
    1.13  (* The threshold should be large enough so that MaSh doesn't kick in for Auto
    1.14     Sledgehammer and Try. *)
    1.15  val min_secs_for_learning = 15
    1.16 -val short_learn_timeout_factor = 0.2
    1.17 -val long_learn_timeout_factor = 4.0
    1.18 +val learn_timeout_factor = 2.0
    1.19  
    1.20  fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
    1.21          max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
    1.22 @@ -597,16 +596,13 @@
    1.23    else
    1.24      let
    1.25        val thy = Proof_Context.theory_of ctxt
    1.26 -      fun maybe_learn can_suggest =
    1.27 +      fun maybe_learn () =
    1.28          if not learn orelse Async_Manager.has_running_threads MaShN then
    1.29            ()
    1.30          else if Time.toSeconds timeout >= min_secs_for_learning then
    1.31            let
    1.32 -            val factor =
    1.33 -              if can_suggest then short_learn_timeout_factor
    1.34 -              else long_learn_timeout_factor
    1.35 -            val soft_timeout = time_mult factor timeout
    1.36 -            val hard_timeout = time_mult 2.0 soft_timeout
    1.37 +            val soft_timeout = time_mult learn_timeout_factor timeout
    1.38 +            val hard_timeout = time_mult 4.0 soft_timeout
    1.39              val birth_time = Time.now ()
    1.40              val death_time = Time.+ (birth_time, hard_timeout)
    1.41              val desc = ("machine learner for Sledgehammer", "")
    1.42 @@ -619,12 +615,10 @@
    1.43            ()
    1.44        val fact_filter =
    1.45          case fact_filter of
    1.46 -          SOME ff =>
    1.47 -          (if ff <> iterN then maybe_learn (mash_can_suggest_facts ctxt)
    1.48 -           else (); ff)
    1.49 +          SOME ff => (() |> ff <> iterN ? maybe_learn; ff)
    1.50          | NONE =>
    1.51 -          if mash_can_suggest_facts ctxt then (maybe_learn true; meshN)
    1.52 -          else if mash_could_suggest_facts () then (maybe_learn false; iterN)
    1.53 +          if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
    1.54 +          else if mash_could_suggest_facts () then (maybe_learn (); iterN)
    1.55            else iterN
    1.56        val add_ths = Attrib.eval_thms ctxt add
    1.57        fun prepend_facts ths accepts =